# HG changeset patch
# User wenzelm
# Date 1271690861 -7200
# Node ID e86d9a10e9822f22f0c5e2c314c95931f6ac4dc9
# Parent  16c371c6ff863ad1c7ddce47db3a165c4592648f
check JVM platform at most once -- still non-strict to prevent potential failure during initialization of object Platform;

diff -r 16c371c6ff86 -r e86d9a10e982 src/Pure/System/gui_setup.scala
--- 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 {
diff -r 16c371c6ff86 -r e86d9a10e982 src/Pure/System/platform.scala
--- 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 {