diff --git a/.ci/Jenkinsfile b/.ci/Jenkinsfile index 6164032..99ddea8 100644 --- a/.ci/Jenkinsfile +++ b/.ci/Jenkinsfile @@ -4,7 +4,7 @@ pipeline { stages { stage('Build PDFs') { steps { - sh 'cd examples && (for i in *.tex; do pdflatex $i; pdflatex $i; pdflatex $i; done)' + sh 'docker run -v $PWD/:/authorarchive logicalhacking:debian4isabelle sh -c "cd /authorarchive/examples && (for i in *.tex; do pdflatex \\$i; pdflatex \\$i; pdflatex \\$i; done)"' } } }