expand all files uniformly;
authorwenzelm
Thu, 23 Aug 2012 13:31:00 +0200
changeset 48904 eaf240e9bdc8
parent 48903 1621b3f26095
child 48905 04576657cf94
expand all files uniformly;
src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Thu Aug 23 13:26:27 2012 +0200
+++ b/src/Pure/System/build.scala	Thu Aug 23 13:31:00 2012 +0200
@@ -357,11 +357,11 @@
           val syntax = thy_deps.make_syntax
 
           val all_files =
-            thy_deps.deps.map({ case (n, h) =>
-              val thy = Path.explode(n.node).expand
-              val uses = h.uses.map(p => (Path.explode(n.dir) + Path.explode(p._1)).expand)
+            (thy_deps.deps.map({ case (n, h) =>
+              val thy = Path.explode(n.node)
+              val uses = h.uses.map(p => Path.explode(n.dir) + Path.explode(p._1))
               thy :: uses
-            }).flatten ::: info.files.map(file => info.dir + file)
+            }).flatten ::: info.files.map(file => info.dir + file)).map(_.expand)
 
           if (list_files)
             echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))