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