diff --git a/Jenkinsfile b/Jenkinsfile index 202616d..77c1cce 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -30,6 +30,7 @@ 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