# HG changeset patch
# User paulson
# Date 843495972 -7200
# Node ID 83db8207c9e5fdb6b7c70d36052edea1fe0bc3ad
# Parent  d4a8fd8a806539e331e030b04a1623b22bc37dfd
Now uses init_html

diff -r d4a8fd8a8065 -r 83db8207c9e5 src/HOL/Auth/Makefile
--- a/src/HOL/Auth/Makefile	Mon Sep 23 18:22:52 1996 +0200
+++ b/src/HOL/Auth/Makefile	Mon Sep 23 18:26:12 1996 +0200
@@ -18,17 +18,17 @@
 	poly*)	echo 'make_database"$(BIN)/Auth"; quit();'  \
 		  | $(COMP) $(BIN)/HOL;\
                 if [ "$${MAKE_HTML}" = "true" ]; \
-                then echo 'open PolyML; make_html := true; exit_use"DB-ROOT.ML";' \
+                then echo 'open PolyML; init_html(); exit_use"DB-ROOT.ML";' \
                        | $(COMP) $(BIN)/Auth;\
 		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-                then echo 'open PolyML; make_html := true; exit_use"DB-ROOT.ML";                               make_html := false;' | $(COMP) $(BIN)/Auth;\
+                then echo 'open PolyML; init_html(); exit_use"DB-ROOT.ML";                               make_html := false;' | $(COMP) $(BIN)/Auth;\
                 else echo 'open PolyML; exit_use"DB-ROOT.ML";' \
                        | $(COMP) $(BIN)/Auth;\
                 fi;;\
 	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
-                then echo 'make_html := true; exit_use"DB-ROOT.ML";                                            xML"$(BIN)/Auth" banner;' | $(BIN)/HOL;\
+                then echo 'init_html(); exit_use"DB-ROOT.ML";                                            xML"$(BIN)/Auth" banner;' | $(BIN)/HOL;\
                 elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
-                then echo 'make_html := true; exit_use"DB-ROOT.ML";                                            make_html := false; xML"$(BIN)/Auth" banner;' \
+                then echo 'init_html(); exit_use"DB-ROOT.ML";                                            make_html := false; xML"$(BIN)/Auth" banner;' \
                        | $(BIN)/HOL;\
                 else echo 'exit_use"DB-ROOT.ML"; xML"$(BIN)/Auth" banner;' \
                        | $(BIN)/HOL;\