contrib/jenkins.sh: run "make maintainer-clean"

Related: OS#3047 Change-Id: I9d9b2412f005e4bda0ed35ba715cfb4dca1b04c1
2019-07-10 12:21:18 +02:00 · 2019-07-10 12:21:18 +02:00 · 04e980dd10
parent 7d1d294807
commit 04e980dd10
1 changed files with 2 additions and 0 deletions
--- a/contrib/jenkins_common.sh
+++ b/contrib/jenkins_common.sh
@ -57,4 +57,6 @@ build_bts() {
    if [ "$WITH_MANUALS" = "1" ] && [ "$PUBLISH" = "1" ]; then
        $MAKE -C "$base/doc/manuals" publish
    fi
+
+    $MAKE maintainer-clean
 }