fixed error message spacing
authorhaftmann
Thu, 15 Jan 2009 14:52:26 +0100
changeset 29497 d828e6ca9c11
parent 29496 d35769eb9fc9
child 29498 49675edf127c
fixed error message spacing
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;