diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1999-10-07 18:16:30 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1999-10-07 18:16:30 +0000 |
| commit | 96b1454b8c3d5695a7306db6df3ec756c335dc2f (patch) | |
| tree | 160d3a21468d853a64c39c7c061955227d58d02c /Makefile.devel | |
| parent | 1e2e96911b57991708197be7245ea3aa6a9c9339 (diff) | |
Fixed PRERELEASE_PREFIX.
Diffstat (limited to 'Makefile.devel')
| -rw-r--r-- | Makefile.devel | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/Makefile.devel b/Makefile.devel index 288dfebe..0d5198c9 100644 --- a/Makefile.devel +++ b/Makefile.devel @@ -49,12 +49,12 @@ ########################################################################### -# Release tag. For pre-releases. Watch out with -# substitution in tag target below, which edits $(DOWNLOADHTML) +# PRERELEASE_PREFIX is used to match PRERELEASE_TAG in sed +# line in tag target below, which edits $(DOWNLOADHTML) +PRERELEASE_PREFIX=3\.0pre PRERELEASE_TAG=3.0pre$(shell date "+%y%m%d") PREREL_TAG_FILE=prereltag.txt -# html/download.phtml DOWNLOADHTML=download.phtml @@ -251,7 +251,7 @@ tag: # Edit $(DOWNLOADHTML) only for prereleases. # Careful: the sed command below relies on previous value of PRERELEASE_TAG. if [ $(PRERELEASE_TAG) = $(VERSION) ]; then \ - (cd html; mv $(DOWNLOADHTML) $(DOWNLOADHTML).old; sed -e 's|ProofGeneral-2\.2pre......|ProofGeneral-$(PRERELEASE_TAG)|g' $(DOWNLOADHTML).old > $(DOWNLOADHTML); rm $(DOWNLOADHTML).old) \ + (cd html; mv $(DOWNLOADHTML) $(DOWNLOADHTML).old; sed -e 's|ProofGeneral-$(PRERELEASE_PREFIX)......|ProofGeneral-$(PRERELEASE_TAG)|g' $(DOWNLOADHTML).old > $(DOWNLOADHTML); rm $(DOWNLOADHTML).old) \ fi # This hack to SOURCE: name is only needed because we have an obsolete version # of rpm installed on standard machines at dcs.ed, and we have to build with |