# HG changeset patch
# User wenzelm
# Date 1604241101 -3600
# Node ID 7cb68b5b103dd32239c7d9a0a4d136825bf9e894
# Parent  e0c6522d5d437b4c021c20d17934cca2e8f8ed37
proper build_call for interpreted ARM platform;

diff -r e0c6522d5d43 -r 7cb68b5b103d src/Pure/General/sha1.ML
--- a/src/Pure/General/sha1.ML	Sun Nov 01 14:30:09 2020 +0100
+++ b/src/Pure/General/sha1.ML	Sun Nov 01 15:31:41 2020 +0100
@@ -148,11 +148,14 @@
 val library_path =
   Path.explode ("$ML_HOME/" ^ (if ML_System.platform_is_windows then "sha1.dll" else "libsha1.so"));
 
-val library_call =
+fun build_call () =
   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 ();
+
 fun with_memory n =
   Thread_Attributes.uninterruptible (fn restore_attributes => fn f =>
     let
diff -r e0c6522d5d43 -r 7cb68b5b103d src/Pure/ML/ml_system.ML
--- a/src/Pure/ML/ml_system.ML	Sun Nov 01 14:30:09 2020 +0100
+++ b/src/Pure/ML/ml_system.ML	Sun Nov 01 15:31:41 2020 +0100
@@ -10,6 +10,7 @@
   val platform: string
   val platform_is_windows: bool
   val platform_is_64: bool
+  val platform_is_arm: bool
   val platform_path: string -> string
   val standard_path: string -> string
 end;
@@ -21,6 +22,7 @@
 val SOME platform = OS.Process.getEnv "ML_PLATFORM";
 val platform_is_windows = String.isSuffix "windows" platform;
 val platform_is_64 = String.isPrefix "x86_64-" platform;
+val platform_is_arm = String.isPrefix "arm64-" platform;
 
 val platform_path =
   if platform_is_windows then