# HG changeset patch
# User paulson
# Date 864998099 -7200
# Node ID 86c0d19886226e6c7658f170de026440b8582d92
# Parent  8f225296fade6fa35478d2026a02ef557c2f15e6
flushOut ensures that no recent error message are lost (not certain this is
necessary)

diff -r 8f225296fade -r 86c0d1988622 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue May 27 17:49:52 1997 +0200
+++ b/src/Pure/library.ML	Fri May 30 15:14:59 1997 +0200
@@ -747,7 +747,9 @@
 		            (TextIO.stdOut, "\n*** " ^ s ^ "\n\n"));
 
 exception ERROR;
-fun error msg = (!error_fn msg; raise ERROR);
+fun error msg = (!error_fn msg;
+		 TextIO.flushOut TextIO.stdOut; 
+		 raise ERROR);
 fun sys_error msg = (!error_fn "*** SYSTEM ERROR ***"; error msg);
 
 fun assert p msg = if p then () else error msg;