added base_path;
authorwenzelm
Tue Jan 13 18:03:37 1998 +0100 (1998-01-13)
changeset 4567b0b963a01a0c
parent 4566 23c01c724d7a
child 4568 7be03035c553
added base_path;
src/Pure/Thy/browser_info.ML
     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