make/jprt.properties
changeset 33926 3a19edba4808
parent 30545 56cccb06d21c
child 33928 d2c9fee88260
--- a/make/jprt.properties	Wed Jul 05 20:36:16 2017 +0200
+++ b/make/jprt.properties	Thu Jun 11 00:21:56 2015 +0200
@@ -93,6 +93,7 @@
     --with-output-sync=recurse 						\
     --with-boot-jdk=$ALT_BOOTDIR 					\
     --with-jobs=$ALT_PARALLEL_COMPILE_JOBS 				\
+    --with-version-opt=$JPRT_JOB_ID					\
     ${my.additional.build.configure.args.${jprt.test.set}}		\
     ${my.custom.build.configure.args}