From ebc5206c4514062d59bf51a317abca53c0eb3139 Mon Sep 17 00:00:00 2001
From: Dany LE <xsang.le@gmail.com>
Date: Tue, 3 Jan 2023 18:05:53 +0100
Subject: [PATCH] Update Jenkinsfile

---
 Jenkinsfile | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Jenkinsfile b/Jenkinsfile
index ed14e7f..a85dc18 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -31,6 +31,9 @@ pipeline{
           buildir="build"
           [ -d "$buildir" ] && rm -rf "$buildir"
           export BUILDDIR="$WORKSPACE/$buildir/opt/www/htdocs/os"
+          [ -d "doc" ] && rm -rf doc
+          mkdir doc
+          export DOCDIR="$WORKSPACE/doc"
           make release
           make doc
         '''