script

Author: marcoieni

src/ci/docker/run.sh

@@ -305,7 +305,7 @@ fi
 # In this way, we run the SCRIPT defined in CI,
 # instead of the one defined in the Dockerfile.
 if [ -n "${SCRIPT+x}" ]; then
-  args="$args --build-arg SCRIPT_ARG=$SCRIPT"
+  args="$args --build-arg SCRIPT_ARG=${SCRIPT}"
 fi
 
 if isCI; then