src/Tools/jEdit/src/jedit_resources.scala
changeset 65361 ecefb68dc21d
parent 65359 9ca34f0407a9
child 65441 9425e4d8bdb6
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Apr 03 16:50:44 2017 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Apr 03 17:00:36 2017 +0200
     1.3 @@ -21,7 +21,8 @@
     1.4  import org.gjt.sp.jedit.bufferio.BufferIORequest
     1.5  
     1.6  
     1.7 -class JEdit_Resources(base: Sessions.Base) extends Resources(session_name = "", base)
     1.8 +class JEdit_Resources(session_base: Sessions.Base)
     1.9 +  extends Resources(session_name = "", session_base)
    1.10  {
    1.11    /* document node name */
    1.12