# HG changeset patch
# User wenzelm
# Date 921681784 -3600
# Node ID ab422f55407481a1b15173b4cdb4c2db1cea6df2
# Parent  3e98baa348ec6d7ace0dc543ca1c50329f217390
tuned msg;

diff -r 3e98baa348ec -r ab422f554074 src/Pure/Thy/browser_info.ML
--- a/src/Pure/Thy/browser_info.ML	Wed Mar 17 13:56:29 1999 +0100
+++ b/src/Pure/Thy/browser_info.ML	Wed Mar 17 15:43:04 1999 +0100
@@ -117,10 +117,8 @@
 
 
 
-
 (** HTML output **)
 
-
 (* maintain index *)
 
 val session_entries =
@@ -140,7 +138,7 @@
 
 fun update_index dir name =
   (case try get_entries dir of
-    None => warning ("Browser info: cannot access session index in " ^ quote (Path.pack dir))
+    None => warning ("Browser info: cannot access session index of " ^ quote (Path.pack dir))
   | Some es => (put_entries ((es \ name) @ [name]) dir; create_index dir));