| changeset 11852 | a528a716a312 |
| parent 5836 | 90f7d9f1a0cc |
| child 13037 | f7f29f8380ce |
--- 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