Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit

Permalink
fix(gitpod): correct command name (#13976)
Browse files Browse the repository at this point in the history
`leanpkg config` doesn't exist, it's `leanpkg configure`.

@b-mehta tricked me in #13949 (comment)
  • Loading branch information
eric-wieser committed May 5, 2022
1 parent 73e5dad commit c12536a
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion .gitpod.yml
Original file line number Diff line number Diff line change
Expand Up @@ -6,5 +6,5 @@ vscode:
- jroesch.lean

tasks:
- init: leanpkg config && leanproject get-cache --fallback=download-all
- init: leanpkg configure && leanproject get-cache --fallback=download-all
command: . /home/gitpod/.profile

0 comments on commit c12536a

Please sign in to comment.