# HG changeset patch
# User wenzelm
# Date 1124192568 -7200
# Node ID f5af929f0fb4b74a2fa41ab8d4bdcdcad9992377
# Parent  c7effdf2e2e29ac71ebbc7f50234c5b95c0e466b
added String.isSuffix;

diff -r c7effdf2e2e2 -r f5af929f0fb4 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Tue Aug 16 13:42:47 2005 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Tue Aug 16 13:42:48 2005 +0200
@@ -8,12 +8,20 @@
 
 (** ML system and platform related **)
 
+(* String compatibility *)
+
+structure String =
+struct
+  fun isSuffix s1 s2 =
+    let val n1 = size s1 and n2 = size s2
+    in if n1 = n2 then s1 = s2 else n1 <= n2 andalso String.substring (s2, n2 - n1, n1) = s1 end;
+  open String;
+end;
+
+
 (* cygwin *)
 
-val cygwin_platform =
-  let val n = size ml_platform
-  in n >= 6 andalso String.substring (ml_platform, n - 6, 6) = "cygwin" end;
-
+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 ();