From c12536a7a1e96489e3dbeb7175ade0c97349df11 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 5 May 2022 19:41:55 +0000 Subject: [PATCH] fix(gitpod): correct command name (#13976) `leanpkg config` doesn't exist, it's `leanpkg configure`. @b-mehta tricked me in https://github.com/leanprover-community/mathlib/pull/13949#issuecomment-1117589670 --- .gitpod.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.gitpod.yml b/.gitpod.yml index c0cac26eda069..7b6772e69ce87 100644 --- a/.gitpod.yml +++ b/.gitpod.yml @@ -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