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 '''