max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: lake: add lake help cache (#10616)

Browse source 
This PR fixes an oversight where `lake cache help` existed but `lake
help cache` (and by extension `lake cache --help`) did not.
This commit is contained in:
Mac Malone 2025-09-29 08:41:28 -04:00 • committed by GitHub
parent 4338a8be32
commit 6f3fef9373
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/lake/Lake/CLI/Help.lean
View file

@ -516,6 +516,7 @@ public def help : (cmd : String) → String
| "pack" => helpPack
| "unpack" => helpUnpack
| "upload" => helpUpload
| "cache" => helpCacheCli
| "test" => helpTest
| "check-test" => helpCheckTest
| "lint" => helpLint