src/Tools/jEdit/src/scala_console.scala
changeset 61558 68b86028e02a
parent 57848 f68cda7c85d4
child 61590 94ab348eaab2
     1.1 --- a/src/Tools/jEdit/src/scala_console.scala	Tue Nov 03 14:03:44 2015 +0100
     1.2 +++ b/src/Tools/jEdit/src/scala_console.scala	Tue Nov 03 16:35:00 2015 +0100
     1.3 @@ -165,7 +165,7 @@
     1.4            }
     1.5            finally {
     1.6              running.change(_ => None)
     1.7 -            Thread.interrupted()
     1.8 +            Thread.interrupted
     1.9            }
    1.10            GUI_Thread.later {
    1.11              if (err != null) err.commandDone()