# HG changeset patch
# User haftmann
# Date 1232027546 -3600
# Node ID d828e6ca9c11f2557c1793a2d7fe9588e4b20aac
# Parent  d35769eb9fc9e33c2c1e8bdb4ea71ee1de5c6c85
fixed error message spacing

diff -r d35769eb9fc9 -r d828e6ca9c11 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Thu Jan 15 14:52:25 2009 +0100
+++ b/src/Pure/Thy/present.ML	Thu Jan 15 14:52:26 2009 +0100
@@ -467,7 +467,7 @@
             val _ = add_file (Path.append html_prefix base_html,
               HTML.ml_file (Url.File base) (File.read path));
             in (Url.File base_html, Url.File raw_path, loadit) end
-      | NONE => error ("Browser info: expected to find ML file" ^ quote (Path.implode raw_path)));
+      | NONE => error ("Browser info: expected to find ML file " ^ quote (Path.implode raw_path)));
 
     val files_html = map prep_file files;