# HG changeset patch # User wenzelm # Date 1604248791 -3600 # Node ID 18eed4f718e00ea4ceefe3ef16fed24fb9f553e9 # Parent 7cb68b5b103dd32239c7d9a0a4d136825bf9e894 back to dynamic library_call: not quite portable, e.g. different Windows installations (see e0c6522d5d43, 7cb68b5b103d) diff -r 7cb68b5b103d -r 18eed4f718e0 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 =>