diff --git a/Jenkinsfile b/Jenkinsfile
index ec42a9946..df6526c6f 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -227,7 +227,8 @@ pipeline
                             when { branch "ruben/jenkins_migration"; }
                             steps
                             {
-                                dir('${env.WORKSPACE}/doc_repo')
+                                
+                                dir("${env.WORKSPACE}/doc_repo")
                                 {
                                     unstash name: 'carla_docs'
                                     withCredentials([gitUsernamePassword(credentialsId: 'github_token_as_pwd_2', gitToolName: 'git-tool')]) {