Zulip Chat Archive
Stream: lean4
Topic: argv[0]
Jason Gross (Mar 19 2021 at 18:32):
Is there any way to get argv[0]
in Lean?
Marc Huisinga (Mar 25 2021 at 13:44):
@Jason Gross If you asked this question because lean4-cli expects the first argument to be the application name while args
does not contain it, I've fixed that in lean4-cli now.
Jason Gross (Mar 25 2021 at 14:31):
No, it was because I'd like to be able to pick up the executable name from argv[0]
for displaying usage messages
Last updated: Dec 20 2023 at 11:08 UTC