src/HOL/Makefile
changeset 2023 aa25f20c5d8b
parent 2019 b45d9f2042e0
child 2091 644104f85d14
     1.1 --- a/src/HOL/Makefile	Tue Sep 24 13:54:27 1996 +0200
     1.2 +++ b/src/HOL/Makefile	Wed Sep 25 11:10:31 1996 +0200
     1.3 @@ -48,7 +48,8 @@
     1.4                  then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/HOL;\
     1.5                  else echo 'open PolyML; exit_use_dir".";' \
     1.6                         | $(COMP) $(BIN)/HOL;\
     1.7 -                fi;;\
     1.8 +                fi;\
     1.9 +		discgarb -c $(BIN)/HOL;;\
    1.10  	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
    1.11                  then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/HOL" banner;' | $(BIN)/Pure;\
    1.12                  elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\