diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/jenkins_common.sh | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/contrib/jenkins_common.sh b/contrib/jenkins_common.sh index fd0359bf..6e4fa7e3 100644 --- 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 } |