src/Tools/jEdit/src/graphview_dockable.scala

--- a/src/Tools/jEdit/src/graphview_dockable.scala	Sun Nov 18 14:24:30 2012 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Sun Nov 18 15:28:58 2012 +0100
@@ -105,7 +105,7 @@
   private val main_actor = actor {
     loop {
       react {
-        case Session.Global_Options =>  // FIXME
+        case _: Session.Global_Options =>  // FIXME
 
         case changed: Session.Commands_Changed =>
           Swing_Thread.later { handle_update(do_update, Some(changed.commands)) }