lean4
lean4 copied to clipboard
`lake translate-config` does not give a helpful error message
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).
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?
Yes, going direct to the help page would be a great solution here.