From fd738bc2d2df80550dddd7cbd2c0fa1c27dfa227 Mon Sep 17 00:00:00 2001 From: Jiri Date: Thu, 21 Dec 2023 12:05:43 +0100 Subject: [PATCH] Made JDK_MAJOR setup-able --- run.sh | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/run.sh b/run.sh index 3db2d88..7546dc7 100755 --- a/run.sh +++ b/run.sh @@ -62,13 +62,16 @@ if [ ! -e "$JTREG_HOME" ] ; then tar -xf $ball fi -JDK_MAJOR=8 -if [[ -e "$JAVA/bin/jshell" || -e "$JAVA/bin/jshell.exe" ]] ; then - jshellScript="$(mktemp)" - printf "System.out.print(Runtime.version().major())\n/exit" > ${jshellScript} - JDK_MAJOR=$( $JAVA/bin/jshell ${jshellScript} 2> /dev/null | grep -v -e "Started recording" -e "copy recording data to file" -e "^$" -e "\[" ) - rm ${jshellScript} +if [ "x$JDK_MAJOR" == "x" ] ; then + JDK_MAJOR=8 + if [[ -e "$JAVA/bin/jshell" || -e "$JAVA/bin/jshell.exe" ]] ; then + jshellScript="$(mktemp)" + printf "System.out.print(Runtime.version().major())\n/exit" > ${jshellScript} + JDK_MAJOR=$( $JAVA/bin/jshell ${jshellScript} 2> /dev/null | grep -v -e "Started recording" -e "copy recording data to file" -e "^$" -e "\[" ) + rm ${jshellScript} + fi fi +echo "treating jdk as: $JDK_MAJOR" JAVA_OPTS=""; if [ "0$JDK_MAJOR" -gt 11 ] ; then