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