Index: Jenkinsfile
===================================================================
--- Jenkinsfile	(revision 8f50da0cd4ada0c4139a97a13838a27d7062504d)
+++ 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
