# HG changeset patch
# User wenzelm
# Date 1555436576 -7200
# Node ID b33f28c81ba9130db712a2d82a53464786001437
# Parent  5389193228528ae2fe5302542848b8be54b2ab36
clarified goto_file (again): treat bad entry as plain file to open empty buffer instead of error (amending a8142ac5e4b6);

diff -r 538919322852 -r b33f28c81ba9 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Sun Apr 14 18:13:46 2019 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Apr 16 19:42:56 2019 +0200
@@ -157,22 +157,22 @@
         }
 
       case None =>
-        val is_file =
+        val is_dir =
           try {
             val vfs = VFSManager.getVFSForPath(name)
             val vfs_file = vfs._getFile((), name, view)
-            vfs_file != null && vfs_file.getType == VFSFile.FILE
+            vfs_file != null && vfs_file.getType == VFSFile.DIRECTORY
           }
           catch { case ERROR(_) => false }
 
-        if (is_file) {
+        if (is_dir) VFSBrowser.browseDirectory(view, name)
+        else {
           val args =
             if (line <= 0) Array(name)
             else if (column <= 0) Array(name, "+line:" + (line + 1))
             else Array(name, "+line:" + (line + 1) + "," + (column + 1))
           jEdit.openFiles(view, null, args)
         }
-        else VFSBrowser.browseDirectory(view, name)
     }
   }