# HG changeset patch
# User paulson
# Date 843642631 -7200
# Node ID aa25f20c5d8b6f93e74a8a66af5c0e6ebcc57612
# Parent  9d47e2962edda979a4c8b406ee5747eade94f031
Calls  discgarb -c  to realize dramatic space savings!

diff -r 9d47e2962edd -r aa25f20c5d8b src/CCL/Makefile
--- a/src/CCL/Makefile	Tue Sep 24 13:54:27 1996 +0200
+++ b/src/CCL/Makefile	Wed Sep 25 11:10:31 1996 +0200
@@ -43,7 +43,8 @@
                 then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/CCL;\
                 else echo 'open PolyML; exit_use_dir".";' \
                        | $(COMP) $(BIN)/CCL;\
-                fi;;\
+                fi;\
+		discgarb -c $(BIN)/CCL;;\
 	sml*)   if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/CCL" banner;' | $(BIN)/FOL;\
                 elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
diff -r 9d47e2962edd -r aa25f20c5d8b src/CTT/Makefile
--- a/src/CTT/Makefile	Tue Sep 24 13:54:27 1996 +0200
+++ b/src/CTT/Makefile	Wed Sep 25 11:10:31 1996 +0200
@@ -42,7 +42,8 @@
                 then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/CTT;\
                 else echo 'open PolyML; exit_use_dir".";' \
                        | $(COMP) $(BIN)/CTT;\
-                fi;;\
+                fi;\
+		discgarb -c $(BIN)/CTT;;\
 	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/CTT" banner;' | $(BIN)/Pure;\
                 elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
diff -r 9d47e2962edd -r aa25f20c5d8b src/Cube/Makefile
--- a/src/Cube/Makefile	Tue Sep 24 13:54:27 1996 +0200
+++ b/src/Cube/Makefile	Wed Sep 25 11:10:31 1996 +0200
@@ -35,7 +35,8 @@
                 then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/Cube;\
                 else echo 'open PolyML; exit_use_dir".";' \
 		       | $(COMP) $(BIN)/Cube;\
-                fi;;\
+                fi;\
+		discgarb -c $(BIN)/Cube;;\
 	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/Cube" banner;' | $(BIN)/Pure;\
                 elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
diff -r 9d47e2962edd -r aa25f20c5d8b src/FOL/Makefile
--- a/src/FOL/Makefile	Tue Sep 24 13:54:27 1996 +0200
+++ b/src/FOL/Makefile	Wed Sep 25 11:10:31 1996 +0200
@@ -45,7 +45,8 @@
                 then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/FOL;\
                 else echo 'open PolyML; exit_use_dir".";' \
                        | $(COMP) $(BIN)/FOL;\
-                fi;;\
+                fi;\
+		discgarb -c $(BIN)/FOL;;\
 	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/FOL" banner;' | $(BIN)/Pure;\
                 elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
diff -r 9d47e2962edd -r aa25f20c5d8b src/FOLP/Makefile
--- a/src/FOLP/Makefile	Tue Sep 24 13:54:27 1996 +0200
+++ b/src/FOLP/Makefile	Wed Sep 25 11:10:31 1996 +0200
@@ -39,7 +39,8 @@
                 then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/FOLP;\
                 else echo 'open PolyML; exit_use_dir".";' \
 		       | $(COMP) $(BIN)/FOLP;\
-                fi;;\
+                fi;\
+		discgarb -c $(BIN)/FOLP;;\
 	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/FOLP" banner;' | $(BIN)/Pure;\
                 elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
diff -r 9d47e2962edd -r aa25f20c5d8b src/HOL/Auth/Makefile
--- a/src/HOL/Auth/Makefile	Tue Sep 24 13:54:27 1996 +0200
+++ b/src/HOL/Auth/Makefile	Wed Sep 25 11:10:31 1996 +0200
@@ -24,7 +24,8 @@
                 then echo 'open PolyML; init_html(); exit_use"DB-ROOT.ML";                               make_html := false;' | $(COMP) $(BIN)/Auth;\
                 else echo 'open PolyML; exit_use"DB-ROOT.ML";' \
                        | $(COMP) $(BIN)/Auth;\
-                fi;;\
+                fi;\
+		discgarb -c $(BIN)/Auth;;\
 	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'init_html(); exit_use"DB-ROOT.ML";                                            xML"$(BIN)/Auth" banner;' | $(BIN)/HOL;\
                 elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
diff -r 9d47e2962edd -r aa25f20c5d8b src/HOL/Makefile
--- a/src/HOL/Makefile	Tue Sep 24 13:54:27 1996 +0200
+++ b/src/HOL/Makefile	Wed Sep 25 11:10:31 1996 +0200
@@ -48,7 +48,8 @@
                 then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/HOL;\
                 else echo 'open PolyML; exit_use_dir".";' \
                        | $(COMP) $(BIN)/HOL;\
-                fi;;\
+                fi;\
+		discgarb -c $(BIN)/HOL;;\
 	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/HOL" banner;' | $(BIN)/Pure;\
                 elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
diff -r 9d47e2962edd -r aa25f20c5d8b src/HOLCF/Makefile
--- a/src/HOLCF/Makefile	Tue Sep 24 13:54:27 1996 +0200
+++ b/src/HOLCF/Makefile	Wed Sep 25 11:10:31 1996 +0200
@@ -43,7 +43,8 @@
                 then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/HOLCF;\
                 else echo 'open PolyML; exit_use_dir".";' \
 		       | $(COMP) $(BIN)/HOLCF;\
-                fi;;\
+                fi;\
+		discgarb -c $(BIN)/HOLCF;;\
 	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/HOLCF" banner;' | $(BIN)/HOL;\
                 elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
diff -r 9d47e2962edd -r aa25f20c5d8b src/LCF/Makefile
--- a/src/LCF/Makefile	Tue Sep 24 13:54:27 1996 +0200
+++ b/src/LCF/Makefile	Wed Sep 25 11:10:31 1996 +0200
@@ -34,7 +34,8 @@
                 then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/LCF;\
                 else echo 'open PolyML; exit_use_dir".";' \
                        | $(COMP) $(BIN)/LCF;\
-                fi;;\
+                fi;\
+		discgarb -c $(BIN)/LCF;;\
 	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/LCF" banner;' | $(BIN)/FOL;\
                 elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
diff -r 9d47e2962edd -r aa25f20c5d8b src/LK/Makefile
--- a/src/LK/Makefile	Tue Sep 24 13:54:27 1996 +0200
+++ b/src/LK/Makefile	Wed Sep 25 11:10:31 1996 +0200
@@ -34,7 +34,8 @@
 		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
                 then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/LK;\
                 else echo 'open PolyML; exit_use_dir".";' | $(COMP) $(BIN)/LK;\
-                fi;;\
+                fi;\
+		discgarb -c $(BIN)/LK;;\
 	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/LK" banner;' | $(BIN)/Pure;\
                 elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
diff -r 9d47e2962edd -r aa25f20c5d8b src/Modal/Makefile
--- a/src/Modal/Makefile	Tue Sep 24 13:54:27 1996 +0200
+++ b/src/Modal/Makefile	Wed Sep 25 11:10:31 1996 +0200
@@ -35,7 +35,8 @@
                 then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/Modal;\
                 else echo 'open PolyML; exit_use_dir".";' \
 		       | $(COMP) $(BIN)/Modal;\
-                fi;;\
+                fi;\
+		discgarb -c $(BIN)/Modal;;\
 	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/Modal" banner;' | $(BIN)/LK;\
                 elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
diff -r 9d47e2962edd -r aa25f20c5d8b src/Pure/Makefile
--- a/src/Pure/Makefile	Tue Sep 24 13:54:27 1996 +0200
+++ b/src/Pure/Makefile	Wed Sep 25 11:10:31 1996 +0200
@@ -41,7 +41,8 @@
 	poly*)	echo database=$${ML_DBASE:?'No Poly/ML database specified'};\
 		cp $(ML_DBASE) $(BIN)/Pure; chmod u+w $(BIN)/Pure;\
 		echo 'PolyML.use"POLY";use"ROOT" handle _=> exit 1;' \
-                  | $(COMP) $(BIN)/Pure;;\
+                  | $(COMP) $(BIN)/Pure;\
+		discgarb -c $(BIN)/Pure;;\
 	sml*)	if [ ! '(' -d $${ISABELLEBIN:?} -a -w $${ISABELLEBIN:?} ')' ];\
            	then echo Bad value for ISABELLEBIN: \
                 	$(BIN) is not a writable directory; \
diff -r 9d47e2962edd -r aa25f20c5d8b src/ZF/Makefile
--- a/src/ZF/Makefile	Tue Sep 24 13:54:27 1996 +0200
+++ b/src/ZF/Makefile	Wed Sep 25 11:10:31 1996 +0200
@@ -44,7 +44,8 @@
                 then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/ZF;\
                 else echo 'open PolyML; exit_use_dir".";' \
                        | $(COMP) $(BIN)/ZF;\
-                fi;;\
+                fi;\
+		discgarb -c $(BIN)/ZF;;\
 	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;\
                 elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\