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