From 782bbd5488e8cdda659dae672e40cb9bbbb24d1c Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 7 Jun 1999 17:06:57 +0000
Subject: Comments

---
 Makefile.devel | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/Makefile.devel b/Makefile.devel
index a46d04f7..5569b3fd 100644
--- a/Makefile.devel
+++ b/Makefile.devel
@@ -12,7 +12,7 @@
 ##
 ##    make ChangeLog	  - make ChangeLog from CVS sources (uses emacs)
 ##    make tag		  - tag the CVS sources with CVS_RELEASENAME
-##    make untag	  - remove tag CVS_RELEASENAME from the sources
+##    make untag	  - remove tag CVS_RELEASENAME from the sources 
 ##    make dist           - make a distribution from sources with above tag
 ##    make rpm		  - make RPM packages based on etc/ProofGeneral.spec
 ##
@@ -26,7 +26,8 @@
 ##
 ##
 ## Notes:
-##   Use 'make untag' before re-trying if 'make releaseall' fails.
+##   Use 'make untag' before re-trying if 'make releaseall' fails and files
+##    are changed. This will make sure tags move to correct files
 ##   Use 'make releaseclean' if giving up, to remove temp dirs.
 ##
 ##   No facility to edit html to make a full release in this makefile.  
-- 
cgit v1.2.3