# HG changeset patch
# User wenzelm
# Date 1547324795 -3600
# Node ID 3694b021e55566b59e0f559839a4205d5c0bbbbf
# Parent  fc2b565fa37725b85dc25da9b6272b32ff816675
avoid access to ".NAME.marks" exports;

diff -r fc2b565fa377 -r 3694b021e555 src/Tools/jEdit/src/isabelle_export.scala
--- 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