From 19cddada2c3960681befcbce2e8d54201676a41f Mon Sep 17 00:00:00 2001
From: Mikael Vidstedt <mikael@openjdk.org>
Date: Tue, 22 Dec 2015 20:47:40 -0800
Subject: [PATCH] 8145828: JPRT hotspot push jobs should allow merge on push

Reviewed-by: dholmes, iklam
---
 make/jprt.properties | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

diff --git a/make/jprt.properties b/make/jprt.properties
index 30d974af888..1d66e76b1ca 100644
--- a/make/jprt.properties
+++ b/make/jprt.properties
@@ -34,13 +34,8 @@ jprt.selective.test.bundle.installation=true
 # 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