# HG changeset patch
# User wenzelm
# Date 1548079826 -3600
# Node ID b5ecabcfb7805f6b46c4d61e77ac425b6ba56c52
# Parent  82f57315cadeabf25ef8f934d6c3ee7d9ae886b2
more operations;

diff -r 82f57315cade -r b5ecabcfb780 src/Pure/ML/ml_system.ML
--- a/src/Pure/ML/ml_system.ML	Sun Jan 20 17:15:49 2019 +0000
+++ b/src/Pure/ML/ml_system.ML	Mon Jan 21 15:10:26 2019 +0100
@@ -9,6 +9,7 @@
   val name: string
   val platform: string
   val platform_is_windows: bool
+  val platform_is_64: bool
   val platform_path: string -> string
   val standard_path: string -> string
 end;
@@ -19,6 +20,7 @@
 val SOME name = OS.Process.getEnv "ML_SYSTEM";
 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_path =
   if platform_is_windows then