diff options
Diffstat (limited to 'dev/make-distribution.sh')
| -rwxr-xr-x | dev/make-distribution.sh | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/dev/make-distribution.sh b/dev/make-distribution.sh index 6ea319e436..6c5ae0d629 100755 --- a/dev/make-distribution.sh +++ b/dev/make-distribution.sh @@ -102,6 +102,13 @@ if [ -z "$JAVA_HOME" ]; then echo "No JAVA_HOME set, proceeding with '$JAVA_HOME' learned from rpm" fi fi + + if [ -z "$JAVA_HOME" ]; then + if [ `command -v java` ]; then + # If java is in /usr/bin/java, we want /usr + JAVA_HOME="$(dirname $(dirname $(which java)))" + fi + fi fi if [ -z "$JAVA_HOME" ]; then |