src/Tools/jEdit/src/syslog_dockable.scala
changeset 57612 990ffb84489b
parent 56775 59f70b89e5fd
child 66591 6efa351190d0
     1.1 --- a/src/Tools/jEdit/src/syslog_dockable.scala	Wed Jul 23 11:08:24 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/syslog_dockable.scala	Wed Jul 23 11:19:24 2014 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4  
     1.5    private val syslog = new TextArea()
     1.6  
     1.7 -  private def syslog_delay = Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay"))
     1.8 +  private def syslog_delay = GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay"))
     1.9    {
    1.10      val text = PIDE.session.syslog_content()
    1.11      if (text != syslog.text) syslog.text = text