--- 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));