Zulip Chat Archive

Stream: lean4

Topic: argv[0]


view this post on Zulip Jason Gross (Mar 19 2021 at 18:32):

Is there any way to get argv[0] in Lean?

view this post on Zulip 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.

view this post on Zulip 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: May 18 2021 at 23:14 UTC