# HG changeset patch # User wenzelm # Date 1605804614 -3600 # Node ID fca4d6abebda1160ce1f6b6fb723ba28788b49bc # Parent 7d4e9f7742c6610fa684fdc59ee531464468fe79 more robust library_call (again): dynamic file name, static symbol; diff -r 7d4e9f7742c6 -r fca4d6abebda src/Pure/General/sha1.ML --- a/src/Pure/General/sha1.ML Thu Nov 19 17:46:58 2020 +0100 +++ b/src/Pure/General/sha1.ML Thu Nov 19 17:50:14 2020 +0100 @@ -150,7 +150,8 @@ val library_call = Foreign.buildCall3 - (Foreign.getSymbol (Foreign.loadLibrary (File.platform_path library_path)) "sha1_buffer", + (Foreign.getSymbol + (Foreign.loadLibraryIndirect (fn () => File.platform_path library_path)) "sha1_buffer", (Foreign.cByteArray, Foreign.cUlong, Foreign.cPointer), Foreign.cPointer); fun with_memory n =