Index: Jenkinsfile
===================================================================
--- Jenkinsfile	(revision f15fe0a1f735a1835eace55776b7074833013644)
+++ Jenkinsfile	(revision d4510ea5e69f9fb30e5931911bbe2411565afb42)
@@ -116,5 +116,5 @@
 			//Also specify the compiler by hand
 			targets=""
-			if( Settings.RunAllTests ) {
+			if( Settings.RunAllTests || Settings.RunBenchmark ) {
 				targets="--with-target-hosts='host:debug,host:nodebug'"
 			} else {