# HG changeset patch
# User wenzelm
# Date 884711017 -3600
# Node ID b0b963a01a0cd17f8d918c2fc01ea418599fb2b3
# Parent  23c01c724d7a47ccb6e1d36ad3ea031e41836708
added base_path;

diff -r 23c01c724d7a -r b0b963a01a0c src/Pure/Thy/browser_info.ML
--- a/src/Pure/Thy/browser_info.ML	Tue Jan 13 14:31:09 1998 +0100
+++ b/src/Pure/Thy/browser_info.ML	Tue Jan 13 18:03:37 1998 +0100
@@ -79,7 +79,7 @@
 sig
   val output_dir       : string ref
   val home_path        : string ref
-
+  val base_path        : string ref
   val make_graph       : bool ref
   val init_graph       : string -> unit
   val mk_graph         : string -> string -> unit