From 3bef4917ad748446eaf554c9410fb04134d19267 Mon Sep 17 00:00:00 2001
From: Matthias Koefferlein <matthias@klayout.de>
Date: Fri, 24 Feb 2023 18:33:24 +0100
Subject: [PATCH] Fixed doc publishing Jenkinsfile

---
 Jenkinsfile-publish-doc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Jenkinsfile-publish-doc b/Jenkinsfile-publish-doc
index 24db16275..619c89019 100644
--- a/Jenkinsfile-publish-doc
+++ b/Jenkinsfile-publish-doc
@@ -10,7 +10,7 @@ node("linux") {
   }
 
   stage("Producing doc") {
-    sh "./scripts/extract_user_doc.sh -i " + BRANCH_NAME
+    linux_sh "./scripts/extract_user_doc.sh -i " + BRANCH_NAME
   }
 
   stage("Publish doc") {