From 6f3fef937359b3ccec3a2817d969212fd92c825c Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Mon, 29 Sep 2025 08:41:28 -0400 Subject: [PATCH] fix: lake: add `lake help cache` (#10616) This PR fixes an oversight where `lake cache help` existed but `lake help cache` (and by extension `lake cache --help`) did not. --- src/lake/Lake/CLI/Help.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/lake/Lake/CLI/Help.lean b/src/lake/Lake/CLI/Help.lean index c431aa7c9b..93cc333566 100644 --- a/src/lake/Lake/CLI/Help.lean +++ b/src/lake/Lake/CLI/Help.lean @@ -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