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

fix: lake: lake cache help put-staged (#13150)

Browse source 
This PR fixes a typo in #13144 where `lake cache help put-staged` was
incorrectly `lake cache help putStaged`.
This commit is contained in:
Mac Malone 2026-03-27 01:11:43 -04:00 • committed by GitHub
parent e55f69acd0
commit 2bc7a77806
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -690,7 +690,7 @@ public def helpCache : (cmd : String) → String
| "add" => helpCacheAdd
| "stage" => helpCacheStage
| "unstage" => helpCacheUnstage
| "putStaged" => helpCachePutStaged
| "put-staged" => helpCachePutStaged
| "clean" => helpCacheClean
| "services" => helpCacheServices
| _ => helpCacheCli