src/Pure/PIDE/rendering.scala
changeset 69366 b6dacf6eabe3
parent 69320 fc221fa79741
child 69648 97ddaec3e2ae
--- a/src/Pure/PIDE/rendering.scala	Wed Nov 28 15:38:18 2018 +0100
+++ b/src/Pure/PIDE/rendering.scala	Wed Nov 28 16:14:31 2018 +0100
@@ -306,7 +306,7 @@
         val path = Path.explode(text)
         val (dir, base_name) =
           if (text == "" || text.endsWith("/")) (path, "")
-          else (path.dir, path.base_name)
+          else (path.dir, path.file_name)
 
         val directory = new JFile(session.resources.append(snapshot.node_name, dir))
         val files = directory.listFiles