Skip to content

Commit c59884f

Browse files
fix(Cache): add put* commands to leanTarArgs (leanprover-community#28164)
Without this, running `lake exe cache put` fails if `leantar` is not already installed. Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
1 parent a26dc25 commit c59884f

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

Cache/Main.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -52,9 +52,9 @@ Valid arguments are:
5252
def curlArgs : List String :=
5353
["get", "get!", "get-", "put", "put!", "put-unpacked", "commit", "commit!"]
5454

55-
/-- Commands which (potentially) call `leantar` for decompressing downloaded files -/
55+
/-- Commands which (potentially) call `leantar` for compressing or decompressing files -/
5656
def leanTarArgs : List String :=
57-
["get", "get!", "pack", "pack!", "unpack", "lookup"]
57+
["get", "get!", "put", "put!", "put-unpacked", "pack", "pack!", "unpack", "lookup"]
5858

5959
/-- Parses an optional `--repo` option. -/
6060
def parseRepo (args : List String) : IO (Option String × List String) := do

0 commit comments

Comments
 (0)