From 6cad71f339577a8c95e3fc84b7ec10545f757b85 Mon Sep 17 00:00:00 2001 From: Stanca Pop Date: Wed, 20 Dec 2023 17:43:52 +0200 Subject: [PATCH] Update Jenkins file --- Jenkinsfile | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Jenkinsfile b/Jenkinsfile index be2eadc..f73b416 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -19,7 +19,8 @@ stage("Build Toolbox") { checkout scm sh 'git submodule update --init' sh 'pip3 install -r ./CI/gen_doc/requirements_doc.txt' - sh 'make -C ./CI/gen_doc doc_ml' + sh 'rm -rf doc || true' + sh 'make -C ./CI/gen_doc doc_ml' sh 'make -C ./CI/scripts build' sh 'make -C ./CI/scripts gen_tlbx' }