# HG changeset patch
# User wenzelm
# Date 1189949817 -7200
# Node ID d5c5d2e13fbf0f13393e85f7c064ee51363ce826
# Parent  425d6445cba6d4ec7fcdd1af3cca3391ac279103
added structure Posix;

diff -r 425d6445cba6 -r d5c5d2e13fbf src/Pure/ML-Systems/proper_int.ML
--- a/src/Pure/ML-Systems/proper_int.ML	Sun Sep 16 15:27:26 2007 +0200
+++ b/src/Pure/ML-Systems/proper_int.ML	Sun Sep 16 15:36:57 2007 +0200
@@ -192,3 +192,19 @@
   open Time;
   fun fmt a b = Time.fmt (dest_int a) b;
 end;
+
+
+(* Posix *)
+
+structure Posix =
+struct
+  open Posix;
+  structure IO =
+  struct
+    open IO;
+    fun mkTextWriter {appendMode, chunkSize, fd, initBlkMode, name} =
+      IO.mkTextWriter {appendMode = appendMode, chunkSize = dest_int chunkSize,
+        fd = fd, initBlkMode = initBlkMode, name = name};
+  end;
+end;
+