src/LCF/Makefile
changeset 2023 aa25f20c5d8b
parent 1491 38a14548baad
child 2094 2061df98aab5
--- 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" ];\