diff options
author | Oliver Smith <osmith@sysmocom.de> | 2019-07-10 12:21:18 +0200 |
---|---|---|
committer | Oliver Smith <osmith@sysmocom.de> | 2019-07-10 13:36:11 +0200 |
commit | 04e980dd10ddb5aac4b0ffeb016162a1291f2c60 (patch) | |
tree | 76c3a77a3a8f13abf236f04ed66a55845647a22b /contrib | |
parent | 7d1d294807ba0acbc710225622095590ef085774 (diff) |
contrib/jenkins.sh: run "make maintainer-clean"
Related: OS#3047
Change-Id: I9d9b2412f005e4bda0ed35ba715cfb4dca1b04c1
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 } |