# HG changeset patch
# User clasohm
# Date 816957636 -3600
# Node ID dc8acbc64062bedaefe3dd4597f4cb47a0550154
# Parent  1c94ebc9089800baf8356fa76576ef9a1a312326
removed make_chart from ROOT.ML;
replaced exit_use by exit_use_dir

diff -r 1c94ebc90898 -r dc8acbc64062 src/FOL/Makefile
--- a/src/FOL/Makefile	Tue Nov 21 12:47:02 1995 +0100
+++ b/src/FOL/Makefile	Tue Nov 21 13:40:36 1995 +0100
@@ -40,13 +40,14 @@
 	poly*)	echo 'make_database"$(BIN)/FOL"; 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)/FOL;\
-		else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/FOL;\
+		else echo 'open PolyML; exit_use_dir".";' \
+                       | $(COMP) $(BIN)/FOL;\
                 fi;;\
 	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
-                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/FOL" banner;' | $(BIN)/Pure;\
-                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/FOL" banner;' \
+                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/FOL" banner;' | $(BIN)/Pure;\
+                else echo 'exit_use_dir"."; xML"$(BIN)/FOL" banner;' \
                        | $(BIN)/Pure;\
                 fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
diff -r 1c94ebc90898 -r dc8acbc64062 src/FOL/ROOT.ML
--- a/src/FOL/ROOT.ML	Tue Nov 21 12:47:02 1995 +0100
+++ b/src/FOL/ROOT.ML	Tue Nov 21 13:40:36 1995 +0100
@@ -72,6 +72,4 @@
 use "../Pure/install_pp.ML";
 print_depth 8;
 
-make_chart ();   (*make HTML chart*)
-
 val FOL_build_completed = ();	(*indicate successful build*)