# HG changeset patch
# User wenzelm
# Date 1137702140 -3600
# Node ID f809deffdd8fec8a85afb553ae37cf1100e46c3d
# Parent  1c310b042d6950b2b255e89efd8d292136fa9207
use: Output.ML_errors;

diff -r 1c310b042d69 -r f809deffdd8f src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Thu Jan 19 21:22:19 2006 +0100
+++ b/src/Pure/General/file.ML	Thu Jan 19 21:22:20 2006 +0100
@@ -147,6 +147,6 @@
 
 (* use ML files *)
 
-val use = Output.toplevel_errors (use o platform_path);
+val use = Output.ML_errors use o platform_path;
 
 end;