make/jprt.properties
changeset 35023 ee10ca0129b2
parent 34600 242c2cfbc666
child 35025 5e007853c06e
--- a/make/jprt.properties	Thu Dec 17 16:20:09 2015 +0300
+++ b/make/jprt.properties	Tue Dec 22 20:47:40 2015 -0800
@@ -34,13 +34,8 @@
 # The current release name
 jprt.tools.default.release=jdk9
 
-# Check if this is the equivalent of a hotspot push job
-# Interpret -testset hotspot to mean exactly that
-my.is.hotspot.job.hotspot=true
-my.is.hotspot.job=${my.is.hotspot.job.${jprt.test.set}}
-
-# Disable syncing the source after builds and tests are done
-jprt.sync.push=${my.is.hotspot.job ? false : true}
+# Allow concurrent changes to be merged in prior to pushing 
+jprt.sync.push=true
 
 # Directories to be excluded from the source bundles
 jprt.bundle.exclude.src.dirs=build dist webrev