# HG changeset patch
# User Eli Zaretskii <eliz@gnu.org>
# Date 1010741956 0
# Node ID e13df10b6b633ba752f862700b70d649b078d85a
# Parent  66ceec02085b95d7a6c1ab923384b4e3ac039ad0
Make version checking in emacs.texi consistent with how we set it there.

diff -r 66ceec02085b -r e13df10b6b63 make-dist
--- a/make-dist	Fri Jan 11 09:15:51 2002 +0000
+++ b/make-dist	Fri Jan 11 09:39:16 2002 +0000
@@ -150,7 +150,7 @@
 
 if [ $update = yes ];
 then
-  if grep -s "GNU Emacs version ${shortversion}" ./man/emacs.texi > /dev/null; then
+  if grep -s "@set EMACSVER  *${shortversion}" ./man/emacs.texi > /dev/null; then
     true
   else
     echo "You must update the version number in \`./man/emacs.texi'"