diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-03-08 09:13:39 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-03-08 09:13:39 +0000 |
| commit | c2a32b2b9fa8979c443d1a6b69ab7d361598cc8c (patch) | |
| tree | c543a8ef31981c752c2a564480a0af1b9dcc001a /Makefile.devel | |
| parent | 0ca1ca25ef08d7f7c3e02a6770d48d73ed4ee91f (diff) | |
Missing semi
Diffstat (limited to 'Makefile.devel')
| -rw-r--r-- | Makefile.devel | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.devel b/Makefile.devel index ae592a63..a5648909 100644 --- a/Makefile.devel +++ b/Makefile.devel @@ -263,7 +263,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-$(PRERELEASE_PREFIX)......|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); \ (cd html; 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 |