From 52ba9a085948a3ceee2d5f4456b529eeddfb8419 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Fri, 15 Nov 2019 03:29:39 -0800 Subject: [PATCH] [opam] Enable user opam switch named differently than compiler Summary: Currently only user-specified opam switches that name compilers are supported. This diff generalizes this so that the switch name and compiler can be specified separately. Reviewed By: jvillard Differential Revision: D18477910 fbshipit-source-id: f17c6363d --- build-infer.sh | 2 +- scripts/opam_utils.sh | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/build-infer.sh b/build-infer.sh index 0ed252157..813dd29d2 100755 --- a/build-infer.sh +++ b/build-infer.sh @@ -121,7 +121,7 @@ fi setup_opam () { opam var root 1>/dev/null 2>/dev/null || opam init --reinit --bare --no-setup - opam_switch_create_if_needed "$INFER_OPAM_SWITCH" + opam_switch_create_if_needed "$INFER_OPAM_SWITCH" "$INFER_OPAM_COMPILER" opam switch set "$INFER_OPAM_SWITCH" } diff --git a/scripts/opam_utils.sh b/scripts/opam_utils.sh index 0c3af420c..07b26be50 100644 --- a/scripts/opam_utils.sh +++ b/scripts/opam_utils.sh @@ -50,6 +50,7 @@ opam_require_version_2 () { # assumes opam is available and initialized opam_switch_create_if_needed () { local switch=$1 + local compiler=$2 local switch_exists=no for installed_switch in $(opam switch list --short); do if [ "$installed_switch" == "$switch" ]; then @@ -58,7 +59,7 @@ opam_switch_create_if_needed () { fi done if [ "$switch_exists" = "no" ]; then - opam switch create "$switch" + opam switch create "$switch" "$compiler" fi }