diff options
author | Richard M. Stallman <[email protected]> | 1993-06-01 22:37:43 +0000 |
---|---|---|
committer | Richard M. Stallman <[email protected]> | 1993-06-01 22:37:43 +0000 |
commit | 7b7a9d23d4b434b694d6d7db4b9cabe0d801a641 (patch) | |
tree | d3ab867295c9ef6fb0f82ef62d585d5bfa7994c7 /make-dist | |
parent | bf3b07d38c36d8c63045e34b75486425502949db (diff) |
Don't hassle me about emacs.texi.
Diffstat (limited to 'make-dist')
-rwxr-xr-x | make-dist | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -73,7 +73,7 @@ if grep -s "GNU Emacs version ${version}" ./man/emacs.texi > /dev/null; then true else echo "You must update the version number in \`./man/emacs.texi'" - exit 1 + sleep 5 fi ### Make sure the subdirectory is available. |