fixed make_html bug
authorclasohm
Fri, 24 Nov 1995 11:46:23 +0100
changeset 1367 78bdb2d04771
parent 1366 3f3c25d3ec04
child 1368 f00280dff0dc
fixed make_html bug
src/HOL/Makefile
--- 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;;\