proper target directory;
authorwenzelm
Sun, 11 Feb 2018 14:21:16 +0100
changeset 67599 544a0293cadc
parent 67598 fb03259692ca
child 67600 d515b6140381
proper target directory;
src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Sun Feb 11 13:50:28 2018 +0100
+++ b/src/Pure/Admin/build_polyml.scala	Sun Feb 11 14:21:16 2018 +0100
@@ -225,8 +225,7 @@
 
     sha1_root match {
       case Some(dir) =>
-        Mercurial.repository(dir).
-          archive(File.standard_path(component + dir + Path.explode("sha1")))
+        Mercurial.repository(dir).archive(File.standard_path(component + Path.explode("sha1")))
       case None =>
     }
   }