# HG changeset patch
# User Glenn Morris <rgm@gnu.org>
# Date 1202502587 0
# Node ID d21e5f7e5b98f80a14fe9fc88a33ba3f872f1105
# Parent  10893c587e90cba6e7f50db71756047fe32a8655
(check-info-dir): New target.

diff -r 10893c587e90 -r d21e5f7e5b98 Makefile.in
--- a/Makefile.in	Fri Feb 08 20:27:28 2008 +0000
+++ b/Makefile.in	Fri Feb 08 20:29:47 2008 +0000
@@ -779,6 +779,24 @@
 	-(cd doc/misc; $(MAKE) $(MFLAGS) info)
 	-(cd doc/lispref; $(MAKE) $(MFLAGS) info)
 	-(cd doc/lispintro; $(MAKE) $(MFLAGS) info)
+
+# The info/dir file must be updated by hand when new manuals are added.
+check-info-dir: info
+	cd info ; \
+	missing= ; \
+	for file in *; do \
+	  test -f "$${file}" || continue ; \
+	  case $${file} in \
+	    *-[0-9]*|COPYING|dir) continue ;; \
+	  esac ; \
+	  grep -q -F ": ($${file})." dir || missing="$${missing} $${file}" ; \
+	done ; \
+	if test -n "$${missing}"; then \
+	  echo "Missing info/dir entries: $${missing}" ; \
+	  exit 1 ; \
+	fi ; \
+	echo "info/dir is OK"
+
 dvi:
 	(cd doc/emacs; $(MAKE) $(MFLAGS) dvi)
 	(cd doc/misc; $(MAKE) $(MFLAGS) dvi)