src/Pure/Thy/browser_info.ML
changeset 4567 b0b963a01a0c
parent 4215 7f7519759b8c
child 4706 c9033f4e0cd0
     1.1 --- a/src/Pure/Thy/browser_info.ML	Tue Jan 13 14:31:09 1998 +0100
     1.2 +++ b/src/Pure/Thy/browser_info.ML	Tue Jan 13 18:03:37 1998 +0100
     1.3 @@ -79,7 +79,7 @@
     1.4  sig
     1.5    val output_dir       : string ref
     1.6    val home_path        : string ref
     1.7 -
     1.8 +  val base_path        : string ref
     1.9    val make_graph       : bool ref
    1.10    val init_graph       : string -> unit
    1.11    val mk_graph         : string -> string -> unit