tree dc5fa075d0a6885f20fc35fe5cdcb5a0887538c5
parent 21034202011d9e6542244176d6e9a4cf5bbd463e
author Stephan Herrmann <stephan.herrmann@berlin.de> 1566936577 +0200
committer Stephan Herrmann <stephan.herrmann@berlin.de> 1566937369 +0200

Releng: make JAVA_HOME configurable from the toplevel jenkins script