src/Tools/jEdit/src/jedit_resources.scala
changeset 65269 2947837b9f04
parent 65243 ba5ce07e06a7
child 65359 9ca34f0407a9
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Mar 15 19:33:34 2017 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Wed Mar 15 19:39:34 2017 +0100
     1.3 @@ -21,11 +21,6 @@
     1.4  import org.gjt.sp.jedit.bufferio.BufferIORequest
     1.5  
     1.6  
     1.7 -object JEdit_Resources
     1.8 -{
     1.9 -  val empty: JEdit_Resources = new JEdit_Resources(Sessions.Base.empty)
    1.10 -}
    1.11 -
    1.12  class JEdit_Resources(base: Sessions.Base) extends Resources(base)
    1.13  {
    1.14    /* document node name */