# HG changeset patch
# User boehmes
# Date 1269380633 -3600
# Node ID d7b3190d8b4a9feac12ba05d65ee1d11eafb27a2
# Parent  ce49d64a98185b812a4645503668b5e897852053
use ml_platform instead of ml_system to distinguish library names

diff -r ce49d64a9818 -r d7b3190d8b4a src/Pure/General/sha1_polyml.ML
--- a/src/Pure/General/sha1_polyml.ML	Tue Mar 23 20:46:47 2010 +0100
+++ b/src/Pure/General/sha1_polyml.ML	Tue Mar 23 22:43:53 2010 +0100
@@ -16,7 +16,7 @@
   in (op ^) (pairself hex_digit (Integer.div_mod (Char.ord c) 16)) end
 
 val lib_path =
-  ("$ML_HOME/" ^ (if String.isSuffix "cygwin" ml_system then "sha1.dll" else "libsha1.so"))
+  ("$ML_HOME/" ^ (if String.isSuffix "cygwin" ml_platform then "sha1.dll" else "libsha1.so"))
   |> Path.explode;
 
 fun digest_external str =