From 72d932f1e9e8ebbf934179fd405cde9404c36fef Mon Sep 17 00:00:00 2001 From: sylvain tricot Date: Wed, 30 Jun 2021 15:34:34 +0200 Subject: [PATCH] work on Jenkinsfile --- Jenkinsfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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...') {