fixed make_html bug
authorclasohm
Fri Nov 24 11:46:23 1995 +0100 (1995-11-24)
changeset 136778bdb2d04771
parent 1366 3f3c25d3ec04
child 1368 f00280dff0dc
fixed make_html bug
src/HOL/Makefile
     1.1 --- a/src/HOL/Makefile	Fri Nov 24 09:27:19 1995 +0100
     1.2 +++ b/src/HOL/Makefile	Fri Nov 24 11:46:23 1995 +0100
     1.3 @@ -47,7 +47,7 @@
     1.4                         | $(COMP) $(BIN)/HOL;\
     1.5                  fi;;\
     1.6  	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
     1.7 -                then echo 'make_html (); exit_use_dir".";                                                 xML"$(BIN)/HOL" banner;' | $(BIN)/Pure;\
     1.8 +                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/HOL" banner;' | $(BIN)/Pure;\
     1.9                  else echo 'exit_use_dir"."; xML"$(BIN)/HOL" banner;' \
    1.10                         | $(BIN)/Pure;\
    1.11                  fi;;\