From 2bc7a778061470e46b4ac882845e8dca34f9550c Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Fri, 27 Mar 2026 01:11:43 -0400 Subject: [PATCH] fix: lake: `lake cache help put-staged` (#13150) This PR fixes a typo in #13144 where `lake cache help put-staged` was incorrectly `lake cache help putStaged`. --- src/lake/Lake/CLI/Help.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/lake/Lake/CLI/Help.lean b/src/lake/Lake/CLI/Help.lean index 8c567cade0..474be93891 100644 --- a/src/lake/Lake/CLI/Help.lean +++ b/src/lake/Lake/CLI/Help.lean @@ -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