diff --git a/download_and_compile.sh b/download_and_compile.sh index 42223d7..6d779a9 100755 --- a/download_and_compile.sh +++ b/download_and_compile.sh @@ -1621,6 +1621,17 @@ ldd "\$@" EndOfScriptText chmod 755 "$SCRIPT" + # Generic wrapper for whatever the user wants to run (ctest, make...) + SCRIPT=run + cat >"$SCRIPT" < $SCRIPT echo "cd \"\$(dirname \"\$0\")\"" >> $SCRIPT