--- 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" ];\
--- 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" ];\
--- 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" ];\
--- 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" ];\
--- 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" ];\
--- 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" ];\
--- 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" ];\
--- 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" ];\
--- 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" ];\
--- 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" ];\
--- 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" ];\
--- 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; \
--- 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" ];\