src/Tools/jEdit/src/jedit_resources.scala
changeset 64856 5e9bf964510a
parent 64854 f5aa712e6250
child 64858 e31cf6eaecb8
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Jan 09 20:31:00 2017 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Jan 09 20:47:45 2017 +0100
     1.3 @@ -23,10 +23,10 @@
     1.4  
     1.5  object JEdit_Resources
     1.6  {
     1.7 -  val empty: JEdit_Resources = new JEdit_Resources(Build.Session_Content.empty)
     1.8 +  val empty: JEdit_Resources = new JEdit_Resources(Sessions.Base.empty)
     1.9  }
    1.10  
    1.11 -class JEdit_Resources(base: Build.Session_Content) extends Resources(base)
    1.12 +class JEdit_Resources(base: Sessions.Base) extends Resources(base)
    1.13  {
    1.14    /* document node name */
    1.15