# HG changeset patch
# User wenzelm
# Date 1538562489 -7200
# Node ID 0012f3a08f4239551dde1b9ad2cb47d458300cff
# Parent  5b749aa452c6c873a4582e5616f2232a04c81953
unused -- avoid illegal access in Java 11;

diff -r 5b749aa452c6 -r 0012f3a08f42 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Wed Oct 03 12:27:39 2018 +0200
+++ b/src/Pure/GUI/gui.scala	Wed Oct 03 12:28:09 2018 +0200
@@ -58,26 +58,6 @@
   }
 
 
-  /* X11 window manager */
-
-  def window_manager(): Option[String] =
-  {
-    if (Platform.is_windows || Platform.is_macos) None
-    else
-      try {
-        val wm =
-          Untyped.method(Class.forName("sun.awt.X11.XWM", true, ClassLoader.getSystemClassLoader),
-            "getWM").invoke(null)
-        if (wm == null) None
-        else Some(wm.toString)
-      }
-      catch {
-        case _: ClassNotFoundException => None
-        case _: NoSuchMethodException => None
-      }
-  }
-
-
   /* simple dialogs */
 
   def scrollable_text(raw_txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false)