Pass --install

leanprover · Apr 17, 2024 · d433172 · d433172
1 parent 9a171ef
commit d433172
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/examples/SubVerso/Examples.lean b/src/examples/SubVerso/Examples.lean
@@ -169,7 +169,7 @@ partial def loadExamples (leanProject : FilePath) : IO (NameMap (NameMap Example
       "ELAN_TOOLCHAIN", "DYLD_LIBRARY_PATH", "LD_LIBRARY_PATH"]
 
   let cmd := "elan"
-  let args := #["run", toolchain, "lake", "build", ":examples"]
+  let args := #["run", "--install", toolchain, "lake", "build", ":examples"]
 
   -- Build the facet
   let res ← IO.Process.output {