# HG changeset patch
# User wenzelm
# Date 1003870441 -7200
# Node ID 6533ceee4cd70c804020e8e3f38946a4b2229a0e
# Parent  8b8923bfc25991e127d35342c390094f48efade7
build option enables most basic browser info (for proper recording of session);

diff -r 8b8923bfc259 -r 6533ceee4cd7 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Tue Oct 23 22:53:08 2001 +0200
+++ b/src/Pure/Thy/present.ML	Tue Oct 23 22:54:01 2001 +0200
@@ -17,7 +17,7 @@
   include BASIC_PRESENT
   val write_graph: {name: string, ID: string, dir: string, unfold: bool,
    path: string, parents: string list} list -> Path.T -> unit
-  val init: bool -> string -> bool -> string list -> string -> Path.T option
+  val init: bool -> bool -> string -> bool -> string list -> string -> Path.T option
     -> Url.T option * bool -> bool -> unit
   val finish: unit -> unit
   val init_theory: string -> unit
@@ -272,8 +272,8 @@
      ("cp " ^ File.sysify_path path1 ^ " " ^ File.sysify_path path2));
 
 
-fun init info doc doc_graph path name doc_prefix2 (remote_path, first_time) verbose =
-  if not info andalso doc = "" andalso is_none doc_prefix2 then
+fun init build info doc doc_graph path name doc_prefix2 (remote_path, first_time) verbose =
+  if not build andalso not info andalso doc = "" andalso is_none doc_prefix2 then
     (browser_info := empty_browser_info; session_info := None)
   else
     let