diff options
| -rw-r--r-- | Makefile.devel | 5 |
1 files 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. |