diff -r c0cb6bd10eec -r 1b0cfb4812d9 src/Tools/jEdit/src/jedit/Plugin.scala --- a/src/Tools/jEdit/src/jedit/Plugin.scala Tue Sep 15 18:14:28 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/Plugin.scala Tue Sep 15 19:01:16 2009 +0200 @@ -164,6 +164,5 @@ // TODO: proper cleanup Isabelle.system = null Isabelle.plugin = null - scala.actors.Scheduler.shutdown() } }