# HG changeset patch # User wenzelm # Date 1494759055 -7200 # Node ID 94cad759001592ed0dadca3bbdab18436f9d63df # Parent 3039d4aa71435abec8070b528c65dfb66524aa3a avoid hardlinks, for more robustness on Windows file-systems; diff -r 3039d4aa7143 -r 94cad7590015 src/Pure/General/mercurial.scala --- a/src/Pure/General/mercurial.scala Sun May 14 12:06:52 2017 +0200 +++ b/src/Pure/General/mercurial.scala Sun May 14 12:50:55 2017 +0200 @@ -68,7 +68,7 @@ case Some(ssh) => ssh.is_dir(root) } if (present) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg } - else clone_repository(source, root, options = "--noupdate", ssh = ssh) + else clone_repository(source, root, options = "--pull --noupdate", ssh = ssh) } class Repository private[Mercurial](root_path: Path, ssh: Option[SSH.Session])