diff --git a/Jenkinsfile b/Jenkinsfile index ec9ed427..654cb429 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -95,7 +95,7 @@ try { stage("publish") { timeout(time: 5, unit: 'MINUTES') { def commit = sh(returnStdout: true, script: "git rev-parse HEAD").trim() def release = env.BRANCH_NAME == "master" || env.BRANCH_NAME == "unstable" || sh(returnStdout: true, script: "git describe --exact-match HEAD || true").trim() - def workDir = pwd() + def workDir = pwd(tmp:true) lock('triqs_publish') { /* Update documention on gh-pages branch */ dir("$workDir/gh-pages") {