diff options
| author | David Aspinall | 1999-06-07 17:06:57 +0000 |
|---|---|---|
| committer | David Aspinall | 1999-06-07 17:06:57 +0000 |
| commit | 782bbd5488e8cdda659dae672e40cb9bbbb24d1c (patch) | |
| tree | cfbc98f31651d366b29d75c2e8df2bda1a5f39a4 /Makefile.devel | |
| parent | 5362a1cccca751562c5e894e9531202b8ac5a36f (diff) | |
Comments
Diffstat (limited to 'Makefile.devel')
| -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. |