# HG changeset patch
# User Richard M. Stallman <rms@gnu.org>
# Date 738974263 0
# Node ID 3f87ded07a678d6fbd70c49fa346ee7a00b41651
# Parent  6cb1311434ba398231b498f09fd0e515245ddd32
Don't hassle me about emacs.texi.

diff -r 6cb1311434ba -r 3f87ded07a67 make-dist
--- a/make-dist	Tue Jun 01 22:26:20 1993 +0000
+++ b/make-dist	Tue Jun 01 22:37:43 1993 +0000
@@ -73,7 +73,7 @@
   true
 else
   echo "You must update the version number in \`./man/emacs.texi'"
-  exit 1
+  sleep 5
 fi
 
 ### Make sure the subdirectory is available.