author | wenzelm |
Wed, 27 Sep 2017 14:48:25 +0200 | |
changeset 66700 | 5174ce7c84f0 |
parent 66699 | 16fd7655d39d |
child 66701 | d181f8a0e857 |
--- a/src/Pure/PIDE/resources.scala Wed Sep 27 13:29:52 2017 +0200 +++ b/src/Pure/PIDE/resources.scala Wed Sep 27 14:48:25 2017 +0200 @@ -66,7 +66,7 @@ val spans = syntax.parse_spans(text) val dir = Path.explode(name.master_dir) spans.iterator.map(Command.span_files(syntax, _)._1).flatten. - map(a => dir + Path.explode(a)).toList + map(a => (dir + Path.explode(a)).expand).toList } else Nil }