clarified: more uniform results;
authorwenzelm
Wed Sep 27 14:48:25 2017 +0200 (19 months ago)
changeset 667005174ce7c84f0
parent 66699 16fd7655d39d
child 66701 d181f8a0e857
clarified: more uniform results;
src/Pure/PIDE/resources.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Wed Sep 27 13:29:52 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Wed Sep 27 14:48:25 2017 +0200
     1.3 @@ -66,7 +66,7 @@
     1.4          val spans = syntax.parse_spans(text)
     1.5          val dir = Path.explode(name.master_dir)
     1.6          spans.iterator.map(Command.span_files(syntax, _)._1).flatten.
     1.7 -          map(a => dir + Path.explode(a)).toList
     1.8 +          map(a => (dir + Path.explode(a)).expand).toList
     1.9        }
    1.10        else Nil
    1.11      }