summaryrefslogtreecommitdiff
path: root/make-dist
diff options
context:
space:
mode:
Diffstat (limited to 'make-dist')
-rwxr-xr-xmake-dist7
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