unset EXTRA

mr-c · mr-c · commit 900921bf3071 · 2018-02-01T14:28:17.000+02:00
diff --git a/jenkins.bash b/jenkins.bash
@@ -43,6 +43,8 @@ do
 	if [[ "$version" = *dev* ]]
 	then
 		EXTRA=" --enable-dev"
+	else
+		EXTRA=""
 	fi
 	if [[ "$CONTAINER" = "singularity" ]]
 	then
