# HG changeset patch
# User clasohm
# Date 817209983 -3600
# Node ID 78bdb2d047710cfe25a0c6d61e2478d2fc4ac1d2
# Parent  3f3c25d3ec04469bfa7d5547696cdec057e55357
fixed make_html bug

diff -r 3f3c25d3ec04 -r 78bdb2d04771 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;;\