src/Tools/jEdit/src/jedit_resources.scala
changeset 66195 bb886f13623a
parent 65532 febfd9f78bd4
child 66574 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 {