author | wenzelm |
Sat, 12 Jan 2019 21:26:35 +0100 | |
changeset 69642 | 3694b021e555 |
parent 69641 | fc2b565fa377 |
child 69643 | 83f15deb2d36 |
--- a/src/Tools/jEdit/src/isabelle_export.scala Sat Jan 12 21:21:35 2019 +0100 +++ b/src/Tools/jEdit/src/isabelle_export.scala Sat Jan 12 21:26:35 2019 +0100 @@ -50,6 +50,8 @@ class VFS extends JEditVFS(vfs_name, vfs_caps) { + override def isMarkersFileSupported: Boolean = false + override def constructPath(parent: String, path: String): String = { if (parent == vfs_prefix || parent.endsWith(Export.sep)) parent + path