diff make-dist @ 8345:cdd772d2e59f

Update the info files.
author Richard M. Stallman <rms@gnu.org>
date Tue, 26 Jul 1994 19:53:49 +0000
parents 686198604dc7
children f7ae124181cd
line wrap: on
line diff
--- a/make-dist	Tue Jul 26 19:47:39 1994 +0000
+++ b/make-dist	Tue Jul 26 19:53:49 1994 +0000
@@ -121,6 +121,10 @@
 ### Update getdate.c.
 (cd lib-src; make -f Makefile getdate.c YACC="bison -y")
 
+echo "Updating Info files."
+
+(cd man; make info)
+
 echo "Updating finder-inf.el."
 
 ### update finder-inf.el.