# HG changeset patch
# User wenzelm
# Date 1003602041 -7200
# Node ID a528a716a31233d3f976fc29444c9e4a43ddb12f
# Parent  d190028f43c50ee959a803b061790756bf9c6924
added TextIO.stdErr;

diff -r d190028f43c5 -r a528a716a312 src/Pure/basis.ML
--- a/src/Pure/basis.ML	Sat Oct 20 20:20:21 2001 +0200
+++ b/src/Pure/basis.ML	Sat Oct 20 20:20:41 2001 +0200
@@ -141,6 +141,7 @@
   exception Io of {name: string, function: string, cause: exn}
   val stdIn 	= std_in
   val stdOut 	= std_out
+  val stdErr 	= std_err
   val openIn 	= open_in
   val openAppend = open_append
   val openOut 	= open_out