minor

lean-dojo · Dec 6, 2023 · a6d987e · a6d987e
1 parent c15dd4a
commit a6d987e
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 2 deletions.
diff --git a/.dockerignore b/.dockerignore
@@ -1,6 +1,5 @@
 *.txt
 .vscode
-build
 tmp
 lake-packages
 .lake

diff --git a/Dockerfile b/Dockerfile
@@ -14,5 +14,5 @@ RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -
 
 # Build the Lean project.
 RUN lake build
-RUN lake script run LeanCopilot/download
+RUN lake exe LeanCopilot/download
 RUN lake build LeanCopilotTests