# HG changeset patch
# User wenzelm
# Date 1389353365 -3600
# Node ID a8af7a9c38d1563f5ebf2cb67aef63f3c936275c
# Parent  bbf2ef613b8ccd235f6de20a157fd9f99a9c61fe
more robust;

diff -r bbf2ef613b8c -r a8af7a9c38d1 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Fri Jan 10 12:05:15 2014 +0100
+++ b/src/Pure/GUI/gui.scala	Fri Jan 10 12:29:25 2014 +0100
@@ -43,19 +43,21 @@
 
   def window_manager(): Option[String] =
   {
-    try {
-      val XWM = Class.forName("sun.awt.X11.XWM", true, ClassLoader.getSystemClassLoader)
-      val getWM = XWM.getDeclaredMethod("getWM")
-      getWM.setAccessible(true)
-      getWM.invoke(null) match {
-        case null => None
-        case wm => Some(wm.toString)
+    if (Platform.is_windows || Platform.is_macos) None
+    else
+      try {
+        val XWM = Class.forName("sun.awt.X11.XWM", true, ClassLoader.getSystemClassLoader)
+        val getWM = XWM.getDeclaredMethod("getWM")
+        getWM.setAccessible(true)
+        getWM.invoke(null) match {
+          case null => None
+          case wm => Some(wm.toString)
+        }
       }
-    }
-    catch {
-      case _: ClassNotFoundException => None
-      case _: NoSuchMethodException => None
-    }
+      catch {
+        case _: ClassNotFoundException => None
+        case _: NoSuchMethodException => None
+      }
   }