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 | |
| parent | 7d1d294807ba0acbc710225622095590ef085774 (diff) | |
contrib/jenkins.sh: run "make maintainer-clean"
Related: OS#3047
Change-Id: I9d9b2412f005e4bda0ed35ba715cfb4dca1b04c1
| -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 } |