Install duneci-install-module.

.gitignore

 /*-stamp
 /base-?/duneci-ctest
+/base-?/duneci-install-module

Makefile

@@ -3,14 +3,17 @@ all: base-8-stamp base-9-stamp dune-2.3-stamp dune-2.4-stamp dune-fufem-stamp du
 clean:
 	rm -f -- ./*-stamp
 	rm -f -- base-8/duneci-ctest base-9/duneci-ctest
+	rm -f -- base-8/duneci-install-module base-9/duneci-install-module
 
-base-8-stamp: base-8/Dockerfile base-common/duneci-ctest
-	cp base-common/duneci-ctest base-8/duneci-ctest
+base-8-stamp: base-8/Dockerfile base-common/duneci-ctest base-common/duneci-install-module
+	cp base-common/duneci-ctest base-8/
+	cp base-common/duneci-install-module base-8/
 	docker build --no-cache -t duneci/base:8 base-8
 	touch $@
 
-base-9-stamp: base-9/Dockerfile base-common/duneci-ctest
-	cp base-common/duneci-ctest base-9/duneci-ctest
+base-9-stamp: base-9/Dockerfile base-common/duneci-ctest base-common/duneci-install-module
+	cp base-common/duneci-ctest base-9/
+	cp base-common/duneci-install-module base-9/
 	docker build --no-cache -t duneci/base:9 base-9
 	touch $@
 

base-8/Dockerfile

@@ -40,3 +40,4 @@ ENV DUNE_CONTROL_PATH=.:/duneci/modules
 ENV PATH=/duneci/bin:$PATH
 COPY opts.clang opts.gcc /duneci/
 COPY duneci-ctest /duneci/bin/
+COPY duneci-install-module /duneci/bin/

base-9/Dockerfile

@@ -40,3 +40,4 @@ ENV DUNE_CONTROL_PATH=.:/duneci/modules
 ENV PATH=/duneci/bin:$PATH
 COPY opts.clang opts.gcc /duneci/
 COPY duneci-ctest /duneci/bin/
+COPY duneci-install-module /duneci/bin/

base-common/duneci-install-module

+#! /bin/bash
+# Author: Ansgar Burchardt <Ansgar.Burchardt@tu-dresden.de>
+
+set -e
+
+usage() {
+    echo "usage: duneci-install-module <Git-repository> <dunecontrol-opts>" >&2
+    exit ${1:-0}
+}
+
+if [[ $# -eq 0 ]]; then
+    usage 0
+fi
+
+repo="${1}"
+module="${repo##*/}"; module="${module%.git}"
+shift
+
+if [[ "${module}" = dune-common ]]; then
+    ln -sf /duneci/modules/dune-common/bin/dunecontrol /duneci/bin
+fi
+
+cd /duneci/modules
+if [[ -d "${module}" ]]; then
+    echo "Module ${module} is already installed." >&2
+    exit 1
+fi
+
+git clone "${repo}"
+dunecontrol --opts=/duneci/opts.gcc "${@}" --only="${module}" all