From cbecb7d3ef14ffc66310a3c54d46a9b884f370f6 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 30 Jun 1999 18:05:29 +0000
Subject: Removed distinstall, doesn't work for temporary server.

---
 Makefile.devel | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/Makefile.devel b/Makefile.devel
index fd73d787..c2baf35f 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 "topdir: $(RPMTOPDIR)" > $(RPMRC)
+#	echo "_rpmdir: $(RPMTOPDIR)" > $(RPMRC)
 	cp -p etc/ProofGeneral.patch $(RPMTOPDIR)/SOURCES
 	cp -p $(DISTBUILDIR)/$(RELEASENAMETARGZ) $(RPMTOPDIR)/SOURCES
 	$(RPM) -ba etc/ProofGeneral.spec
@@ -377,7 +377,10 @@ releaseclean:
 ## releaseall:
 ##     Do everything!
 ##	  
-releaseall: release rpmrelease distinstall releaseclean golive
+##  For now, don't do distinstall any more: this only works 
+##   for the DCS Sun machines.
+## 
+releaseall: release rpmrelease  releaseclean golive
 
 ############################################################
 ##
-- 
cgit v1.2.3