src/Tools/jEdit/src/session_dockable.scala

   private val main_actor = actor {
     loop {
       react {
         case phase: Session.Phase => handle_phase(phase)
 
-        case Session.Global_Options => Swing_Thread.later { logic.load () }
+        case _: Session.Global_Options => Swing_Thread.later { logic.load () }
 
         case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))
 
         case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
       }