# HG changeset patch # User wenzelm # Date 1347650159 -7200 # Node ID 37c1297aa562c4ff989556113a58bc5ac345d267 # Parent c1262d7389fb3bde278aef693fcde385d16230e8 no longer react on global_settings (cf. 34ac36642a31); diff -r c1262d7389fb -r 37c1297aa562 src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Fri Sep 14 20:49:54 2012 +0200 +++ b/src/Tools/jEdit/src/document_view.scala Fri Sep 14 21:15:59 2012 +0200 @@ -363,7 +363,6 @@ text_area.addLeftOfScrollBar(overview) session.raw_edits += main_actor session.commands_changed += main_actor - session.global_settings += main_actor } private def deactivate() @@ -371,7 +370,6 @@ val painter = text_area.getPainter session.raw_edits -= main_actor session.commands_changed -= main_actor - session.global_settings -= main_actor text_area.removeFocusListener(focus_listener) text_area.getView.removeWindowListener(window_listener) painter.removeMouseMotionListener(mouse_motion_listener)