diff --git a/Jenkinsfile b/Jenkinsfile index baf511c..4c0778a 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -3,7 +3,7 @@ pipeline { stages { stage('Building the code...') { steps { - sh 'make devel' + sh 'make devel PYTHON=python3' } } stage('Building HTML documentation...') {