added ' make_html:=false;' to end of ROOT file
authorregensbu
Tue, 12 Mar 1996 12:59:56 +0100
changeset 1571 b4aced335d94
parent 1570 fd1b9c721ac7
child 1572 dbecd983863f
added ' make_html:=false;' to end of ROOT file
src/HOLCF/ROOT.ML
--- a/src/HOLCF/ROOT.ML	Mon Mar 11 23:59:22 1996 +0100
+++ b/src/HOLCF/ROOT.ML	Tue Mar 12 12:59:56 1996 +0100
@@ -39,5 +39,6 @@
 init_pps ();
 
 print_depth 100;  
+make_html:=false;
 
 val HOLCF_build_completed = (); (*indicate successful build*)