diff make-dist @ 3422:3f87ded07a67

Don't hassle me about emacs.texi.
author Richard M. Stallman <rms@gnu.org>
date Tue, 01 Jun 1993 22:37:43 +0000
parents 8e39495c5be4
children cecefb2ab758
line wrap: on
line diff
--- 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.