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}"
|
echo "${bogosities}"
|
||||||
fi
|
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
|
[ $error = yes ] && exit 1
|
||||||
fi
|
fi
|
||||||
|
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue