| changeset 43520 | cec9b95fa35d |
| parent 43282 | 5d294220ca43 |
| child 43661 | 39fdbd814c7f |
--- a/src/Tools/jEdit/src/scala_console.scala Thu Jun 23 14:48:32 2011 +0200 +++ b/src/Tools/jEdit/src/scala_console.scala Thu Jun 23 14:52:32 2011 +0200 @@ -14,6 +14,7 @@ import org.gjt.sp.jedit.{jEdit, JARClassLoader} import org.gjt.sp.jedit.MiscUtilities +import java.lang.System import java.io.{File, OutputStream, Writer, PrintWriter} import scala.tools.nsc.{Interpreter, GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}