refrain from actor shutdown -- slightly low-level;
authorwenzelm
Tue, 15 Sep 2009 19:01:16 +0200
changeset 347351b0cfb4812d9
parent 34734 c0cb6bd10eec
child 34736 a3ad6d51db1d
refrain from actor shutdown -- slightly low-level;
src/Tools/jEdit/src/jedit/Plugin.scala
     1.1 --- a/src/Tools/jEdit/src/jedit/Plugin.scala	Tue Sep 15 18:14:28 2009 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/Plugin.scala	Tue Sep 15 19:01:16 2009 +0200
     1.3 @@ -164,6 +164,5 @@
     1.4      // TODO: proper cleanup
     1.5      Isabelle.system = null
     1.6      Isabelle.plugin = null
     1.7 -    scala.actors.Scheduler.shutdown()
     1.8    }
     1.9  }