commit 213a050dd8b547b203eaa3104872ba50d0e8dbf6
author Stephan Herrmann <stephan.herrmann@berlin.de> Tue Aug 27 22:09:37 2019 +0200
committer Stephan Herrmann <stephan.herrmann@berlin.de> Tue Aug 27 22:22:49 2019 +0200
tree dc5fa075d0a6885f20fc35fe5cdcb5a0887538c5
parent 21034202011d9e6542244176d6e9a4cf5bbd463e

Releng: make JAVA_HOME configurable from the toplevel jenkins script

releng/build-scripts/build/otdt_prerequisites-hipp.sh

diff --git a/releng/build-scripts/build/otdt_prerequisites-hipp.sh b/releng/build-scripts/build/otdt_prerequisites-hipp.sh
index f531553..ba9795c 100644
--- a/releng/build-scripts/build/otdt_prerequisites-hipp.sh
+++ b/releng/build-scripts/build/otdt_prerequisites-hipp.sh
@@ -41,7 +41,7 @@
 PATH=${ANT_HOME}/bin:${PATH}
 
 # Configure Java:
-JAVA_HOME=/shared/common/jdk-9_x64-latest
+JAVA_HOME=${JAVA_HOME:="/shared/common/jdk-9_x64-latest"}
 PATH=${JAVA_HOME}/bin:${PATH}
 
 # EXPORT: additional arguments to pass to Ant: