src/Tools/jEdit/src/jedit_thy_load.scala
changeset 49437 9613780a805b
parent 49424 0d2114eb412a
child 49885 4accee106f0f
     1.1 --- a/src/Tools/jEdit/src/jedit_thy_load.scala	Sat Jul 21 22:13:50 2012 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Sun Jul 22 00:00:22 2012 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4  import org.gjt.sp.jedit.View
     1.5  
     1.6  
     1.7 -class JEdit_Thy_Load extends Thy_Load
     1.8 +class JEdit_Thy_Load extends Thy_Load()
     1.9  {
    1.10    override def append(dir: String, source_path: Path): String =
    1.11    {