jenkins.sh: run 'make distcheck'

Everything is in place for 'make distcheck' now.

(moving manuals to project repositories 18/19)

Related: OS#3385
Change-Id: Ie31fba3d1afd31c25489ce08169101d9ed9de536
This commit is contained in:
Oliver Smith 2018-11-19 11:55:46 +01:00
parent 39bbafbfd7
commit aec8d2b3d8
1 changed files with 1 additions and 0 deletions

View File

@ -10,6 +10,7 @@ autoreconf -fi
./configure
$MAKE $PARALLEL_MAKE
$MAKE $PARALLEL_MAKE check
$MAKE $PARALLEL_MAKE distcheck
if [ "x$publish" = "x--publish" ]; then
mkdir out/