diff options
-rwxr-xr-x | scripts/check_java_home.sh | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/scripts/check_java_home.sh b/scripts/check_java_home.sh index da6113c..36caffe 100755 --- a/scripts/check_java_home.sh +++ b/scripts/check_java_home.sh @@ -4,15 +4,20 @@ set -e if [[ -z "${JAVA_HOME}" ]]; then - echo "error: JAVA_HOME must be set" + echo "JAVA_HOME must be set" exit 1 fi echo "JAVA_HOME is set to: $JAVA_HOME" +if [ ! -f "$JAVA_HOME/bin/java" ]; then + echo "JAVA_HOME does not point to an installation of Java" + exit 1 +fi + java_version=$("$JAVA_HOME/bin/java" -version 2>&1 | sed -n ';s/.* version "\(.*\)\.\(.*\)\..*".*/\1/p;') echo "JAVA_HOME version is: $java_version" if [ "$java_version" -ne 11 ]; then - echo "error: JAVA_HOME must be set to a JDK version 11" + echo "JAVA_HOME must be set to a JDK version 11" exit 1 fi |