# HG changeset patch
# User wenzelm
# Date 1118524686 -7200
# Node ID de1ab9e8ed4f78441e2b98be8c634aaed5687b53
# Parent  f4b7cf8975af47275e330e5c7857cd5bdb024717
Posix patches (from polyml.ML);

diff -r f4b7cf8975af -r de1ab9e8ed4f src/Pure/ML-Systems/polyml-posix.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/polyml-posix.ML	Sat Jun 11 23:18:06 2005 +0200
@@ -0,0 +1,28 @@
+(*  Title:      Pure/ML-Systems/polyml-posix.ML
+    ID:         $Id$
+
+Posix patches for Poly/ML.
+*)
+
+structure OriginalPosix = Posix;
+structure OriginalIO = Posix.IO;
+
+structure Posix =
+struct
+  open OriginalPosix
+  structure IO =
+  struct
+  open OriginalIO
+  val mkTextReader = mkReader
+  val mkTextWriter = mkWriter
+  end;
+end;
+
+(*This extension of the Poly/ML Signal structure is only necessary
+  because in SML/NJ, types Posix.Signal.signal and Signals.signal differ.*)
+structure IsaSignal =
+struct
+  open Signal
+  val usr1 = Posix.Signal.usr1
+  val usr2 = Posix.Signal.usr2
+end;