Add options to the initialisation script.

tools/init_opam_switch.sh

@@ -4,9 +4,39 @@
 #with CDuce PINS
 #Change these variables to suit your needs
 GIT_REPO="git+https://gitlab.math.univ-paris-diderot.fr/cduce/cduce"
-BRANCH="dune-switch"
+BRANCH="devel"
 PACKAGES="cduce-types cduce"
 
+DO_INSTALL=""
+DO_PIN=""
+DO_PRINT=""
+for i in "$@"
+do
+    if test "$i" = "--install"; then
+        DO_INSTALL=1
+    elif test "$i" = "--pin"; then
+        DO_PIN=1
+    elif test "$i" = "--print-deps"; then
+        DO_PRINT=1
+    elif test "$i" = "--help"; then
+        DO_INSTALL=""
+        DO_PIN=""
+        DO_PRINT=""
+        break
+    fi
+done
+
+if test -z "$DO_INSTALL" -a -z "$DO_PIN" -a -z "$DO_PRINT"; then
+    echo "Usage: $0 [options]"
+    echo
+    echo "options:"
+    echo "  --install    install the developpment dependencies via opam"
+    echo "  --pin        execute opam pin add on the git devel branch"
+    echo "  --print-deps print the development dependencies"
+    echo "  --help       display this message"
+    exit 0
+fi
+
 ##
 
 OPAM=`which opam`
@@ -45,6 +75,13 @@ do
     done
     RDEPS="${RDEPS} $q"
 done
-"$OPAM" pin -y --no-action add cduce-types "${GIT_REPO}#${BRANCH}"
-"$OPAM" pin -y --no-action add cduce "${GIT_REPO}#${BRANCH}"
-"$OPAM" install -y $RDEPS
\ No newline at end of file
+if test "$DO_PRINT"; then
+    echo "$RDEPS"
+fi
+if test "$DO_PIN"; then
+    "$OPAM" pin -y --no-action add cduce-types "${GIT_REPO}#${BRANCH}"
+    "$OPAM" pin -y --no-action add cduce "${GIT_REPO}#${BRANCH}"
+fi
+if test "$DO_INSTALL"; then
+"$OPAM" install -y $RDEPS
+fi