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 {