# HG changeset patch
# User wenzelm
# Date 1518355276 -3600
# Node ID 544a0293cadcc8bd56afc247304c3cdbbf3f4639
# Parent  fb03259692cacbf997eb54055ada5a8e7350a01b
proper target directory;

diff -r fb03259692ca -r 544a0293cadc 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 =>
     }
   }