# HG changeset patch
# User wenzelm
# Date 1163114015 -3600
# Node ID 0767e7dad5499df4846c94f7bfd1799318aced5a
# Parent  b4aa7daa506be091628a787ffe9981e103d26adc
no special treatment for cygwin (this is supposed to be actual cygwin, not win32 polyml within cygwin);

diff -r b4aa7daa506b -r 0767e7dad549 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Fri Nov 10 00:12:28 2006 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Fri Nov 10 00:13:35 2006 +0100
@@ -25,13 +25,6 @@
 end;
 
 
-(* cygwin *)
-
-val cygwin_platform = String.isSuffix "cygwin" ml_platform;
-fun if_cygwin f x = if cygwin_platform then f x else ();
-fun unless_cygwin f x = if not cygwin_platform then f x else ();
-
-
 (*low-level pointer equality*)
 val pointer_eq = Address.wordEq;
 
@@ -62,15 +55,10 @@
 
 (* bounded time execution *)
 
-(* FIXME proper implementation available? *)
+(*dummy implementation*)
 fun interrupt_timeout time f x =
   f x;
 
-(*
-unless_cygwin
-  use "ML-Systems/polyml-interrupt-timeout.ML";
-*)
-
 
 (* prompts *)
 
@@ -165,8 +153,7 @@
 
 (** OS related **)
 
-unless_cygwin
-  use "ML-Systems/polyml-posix.ML";
+use "ML-Systems/polyml-posix.ML";
 
 
 (* system command execution *)