lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

RFC: `lake run --help` could explain what a script is

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

It would be nice if reading lake run --help was sufficient to understand how to write a script, and where to put one. It would be fine if it linked to such an explanation rather than including it inline.

kim-em avatar Oct 11 '23 04:10 kim-em

For usability purposes, it might be best if someone other than me updated the help text and PR'd it. My level of familiarity may be disadvantageous in determine what the proper blurb here is. I would be happy to answer any questions in the process.

tydeu avatar Oct 12 '23 20:10 tydeu