diff options
| -rw-r--r-- | Makefile.devel | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Makefile.devel b/Makefile.devel index a99b4f77..16a369ab 100644 --- a/Makefile.devel +++ b/Makefile.devel @@ -348,6 +348,8 @@ tag: # Careful: the sed command below relies on previous value of PRERELEASE_TAG. if [ $(PRERELEASE_TAG) = $(VERSION) ]; then \ (cd $(HTMLDIR); mv $(DOWNLOADHTML) $(DOWNLOADHTML).old; sed -e 's|ProofGeneral-$(PRERELEASE_PREFIX)......|ProofGeneral-$(PRERELEASE_TAG)|g' $(DOWNLOADHTML).old > $(DOWNLOADHTML); rm $(DOWNLOADHTML).old); \ + (cd $(HTMLDIR); mv $(DOWNLOADHTML) $(DOWNLOADHTML).old; sed -e 's|ProofGeneral-emacs-elc-$(PRERELEASE_PREFIX)......|ProofGeneral-emacs-elc-$(PRERELEASE_TAG)|g' $(DOWNLOADHTML).old > $(DOWNLOADHTML); rm $(DOWNLOADHTML).old); \ + (cd $(HTMLDIR); mv $(DOWNLOADHTML) $(DOWNLOADHTML).old; sed -e 's|ProofGeneral-xemacs-elc-$(PRERELEASE_PREFIX)......|ProofGeneral-xemacs-elc-$(PRERELEASE_TAG)|g' $(DOWNLOADHTML).old > $(DOWNLOADHTML); rm $(DOWNLOADHTML).old); \ (cd $(HTMLDIR); mv $(DOWNLOADINFOHTML) $(DOWNLOADINFOHTML).old; sed -e 's|ProofGeneral-$(PRERELEASE_PREFIX)......|ProofGeneral-$(PRERELEASE_TAG)|g' $(DOWNLOADINFOHTML).old > $(DOWNLOADINFOHTML); rm $(DOWNLOADINFOHTML).old) \ fi # This hack to SOURCE: name is only needed because we have an obsolete version |