obsolete;
authorwenzelm
Thu, 20 Aug 2015 19:19:19 +0200
changeset 60989 c967d423953a
parent 60988 1d7a7e33fd67
child 60990 07592e217180
obsolete;
src/Pure/General/sha1_polyml.ML
src/Pure/ML-Systems/ml_system.ML
--- a/src/Pure/General/sha1_polyml.ML	Thu Aug 20 19:15:17 2015 +0200
+++ b/src/Pure/General/sha1_polyml.ML	Thu Aug 20 19:19:19 2015 +0200
@@ -18,9 +18,7 @@
   in (op ^) (apply2 hex_digit (Integer.div_mod (Char.ord c) 16)) end
 
 val lib_path =
-  ("$ML_HOME/" ^
-    (if ML_System.platform_is_cygwin orelse ML_System.platform_is_windows
-     then "sha1.dll" else "libsha1.so"))
+  ("$ML_HOME/" ^ (if ML_System.platform_is_windows then "sha1.dll" else "libsha1.so"))
   |> Path.explode;
 
 val STRING_INPUT_BYTES =
--- a/src/Pure/ML-Systems/ml_system.ML	Thu Aug 20 19:15:17 2015 +0200
+++ b/src/Pure/ML-Systems/ml_system.ML	Thu Aug 20 19:19:19 2015 +0200
@@ -10,7 +10,6 @@
   val is_polyml: bool
   val is_smlnj: bool
   val platform: string
-  val platform_is_cygwin: bool
   val platform_is_windows: bool
   val share_common_data: unit -> unit
   val save_state: string -> unit
@@ -24,7 +23,6 @@
 val is_smlnj = String.isPrefix "smlnj" name;
 
 val SOME platform = OS.Process.getEnv "ML_PLATFORM";
-val platform_is_cygwin = String.isSuffix "cygwin" platform;
 val platform_is_windows = String.isSuffix "windows" platform;
 
 fun share_common_data () = ();