diff -r a7a03f856354 -r 5eca258324ca Admin/PLATFORMS --- a/Admin/PLATFORMS Fri Jan 07 13:24:09 2011 +0100 +++ b/Admin/PLATFORMS Fri Jan 07 15:37:53 2011 +0100 @@ -61,13 +61,13 @@ The ISABELLE_PLATFORM setting variable refers to the 32 bit version of the platform, even on 64 bit hardware. Power-tools need to indicate 64 bit support explicitly, via the (optional) ISABELLE_PLATFORM64 -setting. The following bash expressions prefers the 64 bit platform, +setting. The following bash expression prefers the 64 bit platform, if that is available: "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}" Note that ML and JVM may have a different idea of the platform, -depending the the respective binaries that are actually run. +depending on the respective binaries that are actually run. Dependable system tools