From 0b75954e853c705fd33ca6464dc2d324ce62641d Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 30 Jun 1999 18:08:47 +0000
Subject: topdir stuff broken, to be fixed.

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

diff --git a/Makefile.devel b/Makefile.devel
index c2baf35f..e5b9a3e7 100644
--- a/Makefile.devel
+++ b/Makefile.devel
@@ -350,7 +350,7 @@ release: distclean tag dist develdist
 rpm:	
 	rm -rf $(RPMTOPDIR)
 	mkdir -p $(RPMTOPDIR) $(RPMTOPDIR)/BUILD $(RPMTOPDIR)/SOURCES $(RPMTOPDIR)/SRPMS $(RPMTOPDIR)/RPMS $(RPMTOPDIR)/RPMS/noarch
-#	echo "_rpmdir: $(RPMTOPDIR)" > $(RPMRC)
+	echo "_topdir: $(RPMTOPDIR)" > $(RPMRC)
 	cp -p etc/ProofGeneral.patch $(RPMTOPDIR)/SOURCES
 	cp -p $(DISTBUILDIR)/$(RELEASENAMETARGZ) $(RPMTOPDIR)/SOURCES
 	$(RPM) -ba etc/ProofGeneral.spec
-- 
cgit v1.2.3