From ce40e1027f698868078e68696f857925931ac819 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sat, 22 Jun 2019 16:46:04 +0100 Subject: [PATCH] Added Jenkins configuration. --- .ci/Jenkinsfile | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 .ci/Jenkinsfile diff --git a/.ci/Jenkinsfile b/.ci/Jenkinsfile new file mode 100644 index 0000000..6164032 --- /dev/null +++ b/.ci/Jenkinsfile @@ -0,0 +1,12 @@ +pipeline { + agent any + + stages { + stage('Build PDFs') { + steps { + sh 'cd examples && (for i in *.tex; do pdflatex $i; pdflatex $i; pdflatex $i; done)' + } + } + } +} +