Bug fix

benedikt-schesch · Oct 4, 2023 · d368345 · d368345
1 parent 2c5e12a
commit d368345
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/run.sh b/run.sh
@@ -40,7 +40,7 @@ while [ $# -gt 0 ]; do
   shift
 done
 
-export PATH=$(pwd)/src/scripts/merge_tools/:\$PATH
+export PATH=$(pwd)/src/scripts/merge_tools/:$PATH
 
 mvn -v | head -n 1 | cut -c 14-18 | grep -q 3.9. || { echo "Maven 3.9.* is required"; mvn -v; echo "PATH=$PATH"; exit 1; }
 if [ -z "${JAVA8_HOME:+isset}" ] ; then echo "JAVA8_HOME is not set"; exit 1; fi