check JVM platform at most once -- still non-strict to prevent potential failure during initialization of object Platform;
--- a/src/Pure/System/gui_setup.scala Mon Apr 19 16:04:42 2010 +0200
+++ b/src/Pure/System/gui_setup.scala Mon Apr 19 17:27:41 2010 +0200
@@ -43,7 +43,7 @@
}
// values
- text.append("JVM platform: " + Platform.jvm_platform() + "\n")
+ text.append("JVM platform: " + Platform.jvm_platform + "\n")
if (Platform.is_windows)
text.append("Cygwin root: " + Cygwin.check_root() + "\n")
try {
--- a/src/Pure/System/platform.scala Mon Apr 19 16:04:42 2010 +0200
+++ b/src/Pure/System/platform.scala Mon Apr 19 17:27:41 2010 +0200
@@ -31,7 +31,7 @@
private val Sparc = new Regex("sparc")
private val PPC = new Regex("PowerPC|ppc")
- def jvm_platform(): String =
+ lazy val jvm_platform: String =
{
val arch =
java.lang.System.getProperty("os.arch") match {