Bug fix

benedikt-schesch · Oct 4, 2023 · 79a9b0c · 79a9b0c
1 parent d368345
commit 79a9b0c
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/run.sh b/run.sh
@@ -40,7 +40,8 @@ while [ $# -gt 0 ]; do
   shift
 done
 
-export PATH=$(pwd)/src/scripts/merge_tools/:$PATH
+PATH=$(pwd)/src/scripts/merge_tools/:$PATH
+export 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