# HG changeset patch
# User wenzelm
# Date 1345721460 -7200
# Node ID eaf240e9bdc847606dff48275554d9a35a8aaaa5
# Parent  1621b3f26095fcce523f3bb28e6938a45469b8ba
expand all files uniformly;

diff -r 1621b3f26095 -r eaf240e9bdc8 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("  " + _)))