# HG changeset patch # User huffman # Date 1269396185 25200 # Node ID a336af707767880e088eac6df7503f2d6e77a064 # Parent db69a6a1fbb542547d3908e0e7220964602dc24e# Parent d7b3190d8b4a9feac12ba05d65ee1d11eafb27a2 merged diff -r db69a6a1fbb5 -r a336af707767 src/Pure/General/sha1_polyml.ML --- a/src/Pure/General/sha1_polyml.ML Tue Mar 23 13:42:12 2010 -0700 +++ b/src/Pure/General/sha1_polyml.ML Tue Mar 23 19:03:05 2010 -0700 @@ -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 = @@ -24,7 +24,7 @@ val digest = CInterface.alloc 20 CInterface.Cchar; val _ = CInterface.call3 (CInterface.get_sym (File.platform_path lib_path) "sha1_buffer") - (CInterface.STRING, CInterface.INT, CInterface.POINTER) + (CInterface.STRING, CInterface.LONG, CInterface.POINTER) CInterface.POINTER (str, size str, CInterface.address digest); in fold (suffix o hex_string digest) (0 upto 19) "" end;