author | wenzelm |
Tue, 13 Jan 1998 18:03:37 +0100 | |
changeset 4567 | b0b963a01a0c |
parent 4566 | 23c01c724d7a |
child 4568 | 7be03035c553 |
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