src/HOL/Makefile
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;;\