--- a/src/Tools/jEdit/src/jedit_resources.scala Mon Jan 09 20:31:00 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala Mon Jan 09 20:47:45 2017 +0100
@@ -23,10 +23,10 @@
object JEdit_Resources
{
- val empty: JEdit_Resources = new JEdit_Resources(Build.Session_Content.empty)
+ val empty: JEdit_Resources = new JEdit_Resources(Sessions.Base.empty)
}
-class JEdit_Resources(base: Build.Session_Content) extends Resources(base)
+class JEdit_Resources(base: Sessions.Base) extends Resources(base)
{
/* document node name */