diff options
Diffstat (limited to 'make-dist')
-rwxr-xr-x | make-dist | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/make-dist b/make-dist index 6182b4931a1..31fa53a6f4d 100755 --- a/make-dist +++ b/make-dist @@ -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 |