# HG changeset patch
# User wenzelm
# Date 1313489209 -7200
# Node ID bff7f7afb2db7c32646eb82b42c5191ecae7fa87
# Parent  e5753e2a594483dbe3839e3768360993282135ea
omit MiscUtilities.resolveSymlinks for now -- odd effects on case-insensible file-system;

diff -r e5753e2a5944 -r bff7f7afb2db src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Mon Aug 15 19:42:52 2011 -0700
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Aug 16 12:06:49 2011 +0200
@@ -334,8 +334,8 @@
       else {
         val vfs = VFSManager.getVFSForPath(master_dir)
         if (vfs.isInstanceOf[FileVFS])
-          MiscUtilities.resolveSymlinks(
-            vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
+          vfs.constructPath(master_dir, Isabelle_System.platform_path(path))
+          // FIXME MiscUtilities.resolveSymlinks (!?)
         else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
       }
     }