Nothing is easy. Try a new way to not run leanpkg if it isn't found.

Julian · Oct 20, 2023 · 99a0d93 · 99a0d93
1 parent 9df3a8c
commit 99a0d93
Showing 1 changed file with 6 additions and 2 deletions.
diff --git a/justfile b/justfile
@@ -51,5 +51,9 @@ _clone-test-dependencies: _clean-test-dependencies
 
 # Rebuild some test fixtures used in the test suite.
 _rebuild-test-fixtures:
-    cd "{{ fixtures }}/example-lean3-project/"; {{ if `leanpkg help 2>&1 >/dev/null; echo $?` == "0" { `leanpkg build` } else { "" } }}
-    cd "{{ fixtures }}/example-lean4-project/"; lake build
+    #!/usr/bin/env zsh
+    set -euxo pipefail
+    cd "{{ fixtures }}/example-lean3-project/"
+    leanpkg help 2>&1 >/dev/null && leanpkg build || echo "Lean 3 not found."
+    cd "{{ fixtures }}/example-lean4-project/"
+    lake build