From b289bbd98e048ebb37a0263a9f137c3a10151b1e Mon Sep 17 00:00:00 2001
From: Ellpeck <me@ellpeck.de>
Date: Sun, 16 Apr 2023 13:40:27 +0200
Subject: [PATCH] skip checkout when publishing docs

---
 Jenkinsfile | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Jenkinsfile b/Jenkinsfile
index 048f4d7..0a793e0 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -31,8 +31,9 @@ pipeline {
       }
     }
     stage('Publish Docs') {
-      agent { label 'web' }
       when { branch 'release' }
+      agent { label 'web' }
+      options { skipDefaultCheckout() }
       steps {
         unstash 'site'
         sh 'rm -rf /var/www/MLEM/*'