lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

`lake translate-config` does not give a helpful error message

Open kim-em opened this issue 1 year ago • 2 comments

Currently lake translate-config just says: "error: missing configuration language", but should also say: Try this: lake translate-config toml (or otherwise give a clue about what to do next).

kim-em avatar May 08 '24 02:05 kim-em

I imagine this is a problem with other commands as well? All of them just mention the missing required argument. Perhaps Lake should print out the help page (e.g., lake translate-config --help) for the command?

tydeu avatar May 08 '24 03:05 tydeu

Yes, going direct to the help page would be a great solution here.

kim-em avatar May 08 '24 23:05 kim-em