[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
master
Josh Berdine 5 years ago committed by Facebook Github Bot
parent 64d3abaa24
commit 52ba9a0859

@ -121,7 +121,7 @@ fi
setup_opam () { setup_opam () {
opam var root 1>/dev/null 2>/dev/null || opam init --reinit --bare --no-setup 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" opam switch set "$INFER_OPAM_SWITCH"
} }

@ -50,6 +50,7 @@ opam_require_version_2 () {
# assumes opam is available and initialized # assumes opam is available and initialized
opam_switch_create_if_needed () { opam_switch_create_if_needed () {
local switch=$1 local switch=$1
local compiler=$2
local switch_exists=no local switch_exists=no
for installed_switch in $(opam switch list --short); do for installed_switch in $(opam switch list --short); do
if [ "$installed_switch" == "$switch" ]; then if [ "$installed_switch" == "$switch" ]; then
@ -58,7 +59,7 @@ opam_switch_create_if_needed () {
fi fi
done done
if [ "$switch_exists" = "no" ]; then if [ "$switch_exists" = "no" ]; then
opam switch create "$switch" opam switch create "$switch" "$compiler"
fi fi
} }

Loading…
Cancel
Save