Index: Jenkinsfile
===================================================================
--- Jenkinsfile	(revision cbef27bdc7d00e71d038d831d0fd681904bb5df8)
+++ Jenkinsfile	(revision 8d636496f5398049761b83bb146d0f335a72dc06)
@@ -170,9 +170,5 @@
 	build_stage('Publish') {
 
-		if( !Settings.Publish ) return
-		if( !Settings.RunBenchmark ) {
-			echo 'No results to publish!!!'
-			return
-		}
+		if( !Settings.RunBenchmark ) { echo 'No results to publish!!!' }
 
 		def groupCompile = new PlotGroup('Compilation', 'seconds', true)
@@ -180,8 +176,8 @@
 
 		//Then publish the results
-		do_plot('compile'  , groupCompile    , 'Compilation')
-		do_plot('ctxswitch', groupConcurrency, 'Context Switching')
-		do_plot('mutex'    , groupConcurrency, 'Mutual Exclusion')
-		do_plot('signal'   , groupConcurrency, 'Internal and External Scheduling')
+		do_plot(Settings.RunBenchmark && Settings.Publish, 'compile'  , groupCompile    , 'Compilation')
+		do_plot(Settings.RunBenchmark && Settings.Publish, 'ctxswitch', groupConcurrency, 'Context Switching')
+		do_plot(Settings.RunBenchmark && Settings.Publish, 'mutex'    , groupConcurrency, 'Mutual Exclusion')
+		do_plot(Settings.RunBenchmark && Settings.Publish, 'signal'   , groupConcurrency, 'Internal and External Scheduling')
 	}
 }
@@ -437,9 +433,7 @@
 }
 
-def do_plot(String file, PlotGroup group, String title) {
-	echo "file is ${BuildDir}/benchmark/${file}.csv, group ${group}, title ${title}"
-	dir("${BuildDir}/benchmark/") {
-		plot csvFileName: "cforall-${env.BRANCH_NAME}-${file}.csv",
-			csvSeries: [[
+def do_plot(boolean silent, String file, PlotGroup group, String title) {
+
+	def series = silent ? [] : [[
 				file: "${file}.csv",
 				exclusionValues: '',
@@ -447,5 +441,10 @@
 				inclusionFlag: 'OFF',
 				url: ''
-			]],
+			]];
+
+	echo "file is ${BuildDir}/benchmark/${file}.csv, group ${group}, title ${title}"
+	dir("${BuildDir}/benchmark/") {
+		plot csvFileName: "cforall-${env.BRANCH_NAME}-${file}.csv",
+			csvSeries: series,
 			group: "${group.name}",
 			title: "${title}",