author | wenzelm |
Mon, 26 Dec 2022 19:00:00 +0100 | |
changeset 76782 | a62a609b5db2 |
parent 76781 | d9f48960bf23 |
child 76783 | 8ebde8164bba |
--- 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