From e7fc0a4f10ed7275fc360b6049cf49eead1fb307 Mon Sep 17 00:00:00 2001
From: lemoer <git@irrelefant.net>
Date: Thu, 26 Sep 2019 15:34:01 +0200
Subject: [PATCH] fix typo

---
 contrib/ci/Jenkinsfile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/contrib/ci/Jenkinsfile b/contrib/ci/Jenkinsfile
index 01ae4e08..5ecbe203 100644
--- a/contrib/ci/Jenkinsfile
+++ b/contrib/ci/Jenkinsfile
@@ -13,7 +13,7 @@ pipeline {
         }
         stage('docs') {
             steps {
-                sh' make -C docs html'
+                sh 'make -C docs html'
             }
         }
         stage('build') {