Improve previous make-dist change
* make-dist: Let make check the info files more thoroughly.
This commit is contained in:
parent
129645a7a7
commit
953bf67fbe
1 changed files with 7 additions and 0 deletions
|
@ -281,6 +281,13 @@ if [ $check = yes ]; then
|
|||
echo "${bogosities}"
|
||||
fi
|
||||
|
||||
## This exits with non-zero status if any .info files need
|
||||
## rebuilding.
|
||||
if [ -e Makefile ]; then
|
||||
echo "Checking to see if info files are up-to-date..."
|
||||
make --question info || error=yes
|
||||
fi
|
||||
|
||||
[ $error = yes ] && exit 1
|
||||
fi
|
||||
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue