From 3e4126e37eae4325c87a1f8838ae9f04d53fe209 Mon Sep 17 00:00:00 2001 From: Kate Date: Wed, 7 Jul 2021 15:54:29 +0100 Subject: [PATCH] shell/install.sh: Add the ability to specify the version of opam you want --- shell/install.sh | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/shell/install.sh b/shell/install.sh index 2f13321ba63..400c401a23f 100755 --- a/shell/install.sh +++ b/shell/install.sh @@ -116,6 +116,7 @@ usage() { echo " is from the 2.0 branch already)" echo " --fresh Create the opam $VERSION root from scratch" echo " --restore VERSION Restore a backed up opam binary and root" + echo " --version VERSION Install this specific version instead of $VERSION" echo echo "The default is to backup if the current version of opam is 1.*, or when" echo "using '--fresh' or '--dev'" @@ -135,6 +136,10 @@ while [ $# -gt 0 ]; do if [ $# -lt 2 ]; then echo "Option $1 requires an argument"; exit 2; fi shift; RESTORE=$1;; + --version) + if [ $# -lt 2 ]; then echo "Option $1 requires an argument"; exit 2; fi + shift; + VERSION=$1;; --no-backup) NOBACKUP=1;; --backup)