src/Tools/jEdit/src/jedit_resources.scala
changeset 66195 bb886f13623a
parent 65532 febfd9f78bd4
child 66574 1e5ae735e026
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Jun 26 11:07:48 2017 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Jun 26 15:57:20 2017 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4    /* document node name */
     1.5  
     1.6    def known_file(path: String): Option[Document.Node.Name] =
     1.7 -    JEdit_Lib.check_file(path).flatMap(session_base.known.get_file(_))
     1.8 +    JEdit_Lib.check_file(path).flatMap(session_base.known.get_file(_, bootstrap = true))
     1.9  
    1.10    def node_name(path: String): Document.Node.Name =
    1.11      known_file(path) getOrElse {