From 31f75b386d3f2c42872b4e32cb8c5ad303a2d0f8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Wed, 8 Jan 2025 19:39:34 -0800 Subject: [PATCH] install-deps: fix standalone CI Path to script was wrong, causing a confusing error with sudo --- .docker/build/install-deps.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.docker/build/install-deps.sh b/.docker/build/install-deps.sh index 539b51e9..ecbbbaaa 100755 --- a/.docker/build/install-deps.sh +++ b/.docker/build/install-deps.sh @@ -19,7 +19,7 @@ git clone --branch $FSTAR_BRANCH https://github.com/FStarLang/FStar "$FSTAR_HOME opam install --deps-only "$FSTAR_HOME/fstar.opam" OTHERFLAGS='--admit_smt_queries true' make -j 24 -C "$FSTAR_HOME" -sudo "$FSTAR_HOME/bin/get_fstar_z3.sh" "/usr/local/bin" +sudo "$FSTAR_HOME/.scripts/get_fstar_z3.sh" "/usr/local/bin" # Install other deps "$build_home"/install-other-deps.sh