# HG changeset patch
# User clasohm
# Date 816958007 -3600
# Node ID dac9989eb88fa337d9d0662ac35a8b6d96ae76b5
# Parent  dc8acbc64062bedaefe3dd4597f4cb47a0550154
replaced exit_use by exit_use_dir

diff -r dc8acbc64062 -r dac9989eb88f src/HOL/Makefile
--- a/src/HOL/Makefile	Tue Nov 21 13:40:36 1995 +0100
+++ b/src/HOL/Makefile	Tue Nov 21 13:46:47 1995 +0100
@@ -41,13 +41,14 @@
 	poly*)	echo 'make_database"$(BIN)/HOL"; quit();'  \
 		  | $(COMP) $(BIN)/Pure;\
 		if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
                   | $(COMP) $(BIN)/HOL;\
-		else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/HOL;\
+		else echo 'open PolyML; exit_use_dir".";' \
+                       | $(COMP) $(BIN)/HOL;\
                 fi;;\
 	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
-                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/HOL" banner;' | $(BIN)/Pure;\
-                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/HOL" banner;' \
+                then echo 'make_html (); exit_use_dir".";                                                 xML"$(BIN)/HOL" banner;' | $(BIN)/Pure;\
+                else echo 'exit_use_dir"."; xML"$(BIN)/HOL" banner;' \
                        | $(BIN)/Pure;\
                 fi;;\
 	*)	echo Bad value for ISABELLECOMP: \