Index: Jenkinsfile
===================================================================
--- Jenkinsfile	(revision 50f2cfc94df0631c9195e7875ced72ba1c18c18e)
+++ Jenkinsfile	(revision 56d138e05af78c7a4e2075db733142726de91842)
@@ -262,5 +262,5 @@
 		// Build outside of the src tree to ease cleaning
 		sh "mkdir -p build"
-		dir ('build')
+		dir ('build') {
 			//Configure the conpilation (Output is not relevant)
 			//Use the current directory as the installation target so nothing escapes the sandbox
