diff --git a/build-infer.sh b/build-infer.sh index 813dd29d2..678559266 100755 --- a/build-infer.sh +++ b/build-infer.sh @@ -18,7 +18,9 @@ PLATFORM="$(uname)" SANDCASTLE=${SANDCASTLE:-} NCPU="$(getconf _NPROCESSORS_ONLN 2>/dev/null || echo 1)" INFER_OPAM_DEFAULT_SWITCH="ocaml-variants.4.07.1+flambda" +INFER_OPAM_DEFAULT_COMPILER="$INFER_OPAM_DEFAULT_SWITCH" INFER_OPAM_SWITCH=${INFER_OPAM_SWITCH:-$INFER_OPAM_DEFAULT_SWITCH} +INFER_OPAM_COMPILER=${INFER_OPAM_COMPILER:-$INFER_OPAM_DEFAULT_COMPILER} function usage() { echo "Usage: $0 [-y] [targets]"