make/jprt.properties
changeset 34600 242c2cfbc666
parent 34599 d4e9a69a3cf8
parent 33953 7e7d0a4c718b
child 35023 ee10ca0129b2
child 34602 3c97348e9814
--- a/make/jprt.properties	Mon Dec 07 17:05:03 2015 -0800
+++ b/make/jprt.properties	Tue Dec 08 03:16:58 2015 +0100
@@ -101,10 +101,11 @@
 # Configure args common to all builds
 # Also allows for additional, testset specific configure arguments to be set
 jprt.build.configure.args=						\
-    --with-output-sync=recurse 						\
-    --with-boot-jdk=$ALT_BOOTDIR 					\
-    --with-jobs=$ALT_PARALLEL_COMPILE_JOBS 				\
-    MAKE=$JPRT_MAKE							\
+    --with-output-sync=recurse						\
+    --with-boot-jdk=$ALT_BOOTDIR					\
+    --with-jobs=$ALT_PARALLEL_COMPILE_JOBS				\
+    --with-version-opt=$JPRT_JOB_ID				 	\
+    MAKE=$JPRT_MAKE                                                     \
     ${my.additional.build.configure.args.${jprt.test.set}}		\
     ${my.custom.build.configure.args}