# HG changeset patch
# User wenzelm
# Date 1672077600 -3600
# Node ID a62a609b5db2fb274af7a25aca262adc0f2c2d7b
# Parent  d9f48960bf23ff57edbcaa5d18edf17b506171f4
more robust;

diff -r d9f48960bf23 -r a62a609b5db2 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Dec 26 18:41:27 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Dec 26 19:00:00 2022 +0100
@@ -59,10 +59,10 @@
   }
 
 
-  /* files */
+  /* plain files */
 
   def is_file(name: String): Boolean =
-    VFSManager.getVFSForPath(name).isInstanceOf[FileVFS]
+    name != null && name.nonEmpty && VFSManager.getVFSForPath(name).isInstanceOf[FileVFS]
 
   def check_file(name: String): Option[JFile] =
     if (is_file(name)) Some(new JFile(name)) else None