diff options
| -rwxr-xr-x | make-distribution.sh | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/make-distribution.sh b/make-distribution.sh index 6f708e0ebf..86868438e7 100755 --- a/make-distribution.sh +++ b/make-distribution.sh @@ -85,6 +85,17 @@ while (( "$#" )); do done if [ -z "$JAVA_HOME" ]; then + # Fall back on JAVA_HOME from rpm, if found + if which rpm &>/dev/null; then + RPM_JAVA_HOME=$(rpm -E %java_home 2>/dev/null) + if [ "$RPM_JAVA_HOME" != "%java_home" ]; then + JAVA_HOME=$RPM_JAVA_HOME + echo "No JAVA_HOME set, proceeding with '$JAVA_HOME' learned from rpm" + fi + fi +fi + +if [ -z "$JAVA_HOME" ]; then echo "Error: JAVA_HOME is not set, cannot proceed." exit -1 fi |