From d433172f093c0c1a2760efabcd166cf7c2fa05f8 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 17 Apr 2024 14:31:05 +0200 Subject: [PATCH] Pass --install --- src/examples/SubVerso/Examples.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/examples/SubVerso/Examples.lean b/src/examples/SubVerso/Examples.lean index e412185..74dc74c 100644 --- 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 {