diff options
Diffstat (limited to 'Makefile.devel')
| -rw-r--r-- | Makefile.devel | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.devel b/Makefile.devel index 762cd7bb..dbd439bb 100644 --- a/Makefile.devel +++ b/Makefile.devel @@ -51,7 +51,7 @@ # Release tag. For pre-releases. Watch out with # substitution in tag target below, which edits $(DOWNLOADHTML) -PRERELEASE_TAG=2.1pre$(shell date "+%y%m%d") +PRERELEASE_TAG=2.2pre$(shell date "+%y%m%d") PREREL_TAG_FILE=prereltag.txt # html/download.phtml @@ -243,7 +243,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\.1pre......|ProofGeneral-$(PRERELEASE_TAG)|g' $(DOWNLOADHTML).old > $(DOWNLOADHTML); rm $(DOWNLOADHTML).old) \ + (cd html; mv $(DOWNLOADHTML) $(DOWNLOADHTML).old; sed -e 's|ProofGeneral-2\.2pre......|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 |