From c2a32b2b9fa8979c443d1a6b69ab7d361598cc8c Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 8 Mar 2000 09:13:39 +0000
Subject: Missing semi

---
 Makefile.devel | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
-- 
cgit v1.2.3