[CI] Fix whitespace and style in docs.jenkinsfile

2026-09-06 22:01:29 +00:00 · 2020-11-04 15:34:14 +01:00
parent ed4e3f48e3
commit 79ce612793
1 changed files with 9 additions and 9 deletions
@@ -1,12 +1,12 @@
 pipeline {
-        agent {
-              dockerfile { filename '.ci/ubuntu18.04.dockerfile' }
-        }
-        stages {
-                stage('Build') {
-                    steps {
-                        sh 'make -C Documentation html SPHINXOPTS="-W"'
-                    }
-                }
+    agent {
+        dockerfile { filename '.ci/ubuntu18.04.dockerfile' }
+    }
+    stages {
+        stage('build') {
+            steps {
+                sh 'make -C Documentation html SPHINXOPTS="-W"'
+            }
        }
+    }
 }