# HG changeset patch
# User wenzelm
# Date 1478008790 -3600
# Node ID cdbfa9f64110e6330a6804cb87f614e2a2cc6cb2
# Parent  73859eb8d1fe719301b64994f49dec27f8d7cca0
clarified setup_repository: even more uniform pull vs. clone (see also e84cba30d7ff);

diff -r 73859eb8d1fe -r cdbfa9f64110 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Tue Nov 01 01:25:54 2016 +0100
+++ b/src/Pure/General/mercurial.scala	Tue Nov 01 14:59:50 2016 +0100
@@ -54,7 +54,7 @@
         case None => root.is_dir
         case Some(ssh) => ssh.is_dir(root)
       }
-    if (present) { val hg = repository(root, ssh = ssh); hg.pull(); hg }
+    if (present) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg }
     else clone_repository(source, root, options = "--noupdate", ssh = ssh)
   }