changeset 1367 | 78bdb2d04771 |
parent 1357 | dac9989eb88f |
child 1472 | a89803e3d1bd |
--- a/src/HOL/Makefile Fri Nov 24 09:27:19 1995 +0100 +++ b/src/HOL/Makefile Fri Nov 24 11:46:23 1995 +0100 @@ -47,7 +47,7 @@ | $(COMP) $(BIN)/HOL;\ fi;;\ sml*) if [ "$${MAKE_HTML-undefined}" != "undefined" ];\ - then echo 'make_html (); exit_use_dir"."; xML"$(BIN)/HOL" banner;' | $(BIN)/Pure;\ + then echo 'make_html := true; exit_use_dir"."; xML"$(BIN)/HOL" banner;' | $(BIN)/Pure;\ else echo 'exit_use_dir"."; xML"$(BIN)/HOL" banner;' \ | $(BIN)/Pure;\ fi;;\