back to dynamic library_call: not quite portable, e.g. different Windows installations (see e0c6522d5d43, 7cb68b5b103d)
authorwenzelm
Sun, 01 Nov 2020 17:39:51 +0100
changeset 72537 18eed4f718e0
parent 72535 7cb68b5b103d
child 72538 8f6df3fa7f72
back to dynamic library_call: not quite portable, e.g. different Windows installations (see e0c6522d5d43, 7cb68b5b103d)
src/Pure/General/sha1.ML
--- a/src/Pure/General/sha1.ML	Sun Nov 01 15:31:41 2020 +0100
+++ b/src/Pure/General/sha1.ML	Sun Nov 01 17:39:51 2020 +0100
@@ -148,13 +148,10 @@
 val library_path =
   Path.explode ("$ML_HOME/" ^ (if ML_System.platform_is_windows then "sha1.dll" else "libsha1.so"));
 
-fun build_call () =
+fun library_call args =
   Foreign.buildCall3
     (Foreign.getSymbol (Foreign.loadLibrary (File.platform_path library_path)) "sha1_buffer",
-      (Foreign.cByteArray, Foreign.cUlong, Foreign.cPointer), Foreign.cPointer);
-
-val library_call =
-  if ML_System.platform_is_arm then fn args => build_call () args else build_call ();
+      (Foreign.cByteArray, Foreign.cUlong, Foreign.cPointer), Foreign.cPointer) args;
 
 fun with_memory n =
   Thread_Attributes.uninterruptible (fn restore_attributes => fn f =>