diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-07-18 13:11:08 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-07-18 13:11:08 +0000 |
| commit | 46c6cf124894b0ddbb3a1a1a93aab5ccc3d2eee6 (patch) | |
| tree | ed3ea3938e448f5f762acde8812c0c4949e0238a /Makefile.devel | |
| parent | d272fd5b6bbe0577fb4756dc0392126519a0ec3d (diff) | |
Try to fix latest link
Diffstat (limited to 'Makefile.devel')
| -rw-r--r-- | Makefile.devel | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/Makefile.devel b/Makefile.devel index f6f581fb..804ed8b3 100644 --- a/Makefile.devel +++ b/Makefile.devel @@ -95,6 +95,12 @@ VERSION=$(PRERELEASE_TAG) DATEMSG=$(shell if [ $(PRERELEASE_TAG) = $(VERSION) ]; then echo; else date "+ on %a %e %b %Y"; fi) +# devel just means developer's package, with more files. +# bit ambiguous: "development version" means latest version, +# in development. +# LATESTNAME is linked to the development version. +# NAME is linked to the current release. +# (Before 3.4, NAME was linked to the development version). NAME = ProofGeneral LATESTNAME = $(NAME)-latest DEVELLATESTNAME = $(NAME)-devel-latest @@ -427,11 +433,11 @@ release: distclean tag dist develdist # clean source dir (remove link to this release) (cd $(DISTBUILDIR); rm -f $(NAME)) # clean target dir (remove link for latest release) - (cd $(RELEASEDIR); rm -f $(LASTESTNAME); rm -rf $(RELEASENAME)) + (cd $(RELEASEDIR); rm -rf $(RELEASENAME)) # Seem to need R instead of r here now, # Otherwise cp tries to make hard link instead of symlink?! cp -pfdR $(DISTBUILDIR)/* $(RELEASEDIR) - (cd $(RELEASEDIR); ln -s $(RELEASENAME) $(LATESTNAME)) + (cd $(RELEASEDIR); rm -f $(LATESTNAME); ln -s $(RELEASENAME) $(LATESTNAME)) (cd $(RELEASEDIR); ln -sf $(RELEASENAMETARGZ) $(LATESTNAME).tar.gz) (cd $(RELEASEDIR); ln -sf $(RELEASENAMEZIP) $(LATESTNAME).zip) (cd $(RELEASEDIR); ln -sf $(RELEASENAME)-1.noarch.rpm $(LATESTNAME).noarch.rpm) |