diff options
author | Oliver Smith <osmith@sysmocom.de> | 2019-07-10 13:23:24 +0200 |
---|---|---|
committer | laforge <laforge@gnumonks.org> | 2019-07-11 03:38:37 +0000 |
commit | 5c3a9880cadc29ab8f4354ad2205563ab51201d7 (patch) | |
tree | a794e4d657b8b1c85aa9e63e5f8f3ffc1f7078be | |
parent | e4e70d052e4b28f2d31539d9141df3a0717ff357 (diff) |
contrib/jenkins.sh: run "make maintainer-clean"
Related: OS#3047
Change-Id: I733df8f8bfaf448a6507c9c9d75d2f076fedb342
-rwxr-xr-x | contrib/jenkins.sh | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/contrib/jenkins.sh b/contrib/jenkins.sh index e805080e..8c32cbb9 100755 --- a/contrib/jenkins.sh +++ b/contrib/jenkins.sh @@ -104,4 +104,5 @@ if [ "$WITH_MANUALS" = "1" ] && [ "$PUBLISH" = "1" ]; then make -C "$base/doc/manuals" publish fi +$MAKE maintainer-clean osmo-clean-workspace.sh |