diff options
author | Glenn Morris <rgm@gnu.org> | 2016-12-07 19:43:36 -0500 |
---|---|---|
committer | Glenn Morris <rgm@gnu.org> | 2016-12-07 19:43:36 -0500 |
commit | 953bf67fbea6298cb68b7610fdc09c3fcdf8aeec (patch) | |
tree | 20efbc67ff34e46b642a44f1ffdd68f0d6e6cfc0 /make-dist | |
parent | 129645a7a7129f2a63c1daf2743c2d901460b9fa (diff) | |
download | emacs-953bf67fbea6298cb68b7610fdc09c3fcdf8aeec.tar.gz |
Improve previous make-dist change
* make-dist: Let make check the info files more thoroughly.
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 |