author | clasohm |
Fri, 24 Nov 1995 11:46:23 +0100 | |
changeset 1367 | 78bdb2d04771 |
parent 1366 | 3f3c25d3ec04 |
child 1368 | f00280dff0dc |
src/HOL/Makefile | file | annotate | diff | comparison | revisions |
--- 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;;\