src/Tools/jEdit/src/jedit_resources.scala
changeset 65441 9425e4d8bdb6
parent 65361 ecefb68dc21d
child 65452 9e9750a7932c
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Sat Apr 08 12:47:34 2017 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Sat Apr 08 20:56:41 2017 +0200
     1.3 @@ -21,8 +21,7 @@
     1.4  import org.gjt.sp.jedit.bufferio.BufferIORequest
     1.5  
     1.6  
     1.7 -class JEdit_Resources(session_base: Sessions.Base)
     1.8 -  extends Resources(session_name = "", session_base)
     1.9 +class JEdit_Resources(session_base: Sessions.Base) extends Resources(session_base)
    1.10  {
    1.11    /* document node name */
    1.12