From 5c760037b77dceb826ca99f8e197ba9dca394981 Mon Sep 17 00:00:00 2001
From: Dylan Simon <dylan@dylex.net>
Date: Tue, 14 Jan 2020 15:49:38 -0500
Subject: [PATCH] [jenkins] stage publication results in tmpdir

Currently they're polluting the main build dir and not getting cleaned
up for some reason
---
 Jenkinsfile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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") {