# HG changeset patch
# User wenzelm
# Date 1476617221 -7200
# Node ID e84cba30d7ff3d71edd430d32f167b29be5c3c63
# Parent  528381eb8a7bad00d2b862726ef7a1dd5063747b
clarified setup_repository: more uniform pull vs. clone, without update;

diff -r 528381eb8a7b -r e84cba30d7ff src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Sun Oct 16 13:11:47 2016 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sun Oct 16 13:27:01 2016 +0200
@@ -40,12 +40,7 @@
     Logger_Task("isabelle_identify", logger =>
       {
         val isabelle_id = Mercurial.repository(isabelle_repos).id()
-        val afp_id =
-        {
-          val hg = Mercurial.setup_repository(afp_source, afp_repos)
-          hg.pull()
-          hg.id()
-        }
+        val afp_id = Mercurial.setup_repository(afp_source, afp_repos).id()
 
         File.write(logger.log_dir + Build_Log.log_filename("isabelle_identify", logger.start_date),
           terminate_lines(
diff -r 528381eb8a7b -r e84cba30d7ff src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Sun Oct 16 13:11:47 2016 +0200
+++ b/src/Pure/General/mercurial.scala	Sun Oct 16 13:27:01 2016 +0200
@@ -40,13 +40,15 @@
   }
 
   def setup_repository(source: String, root: Path, ssh: Option[SSH.Session] = None): Repository =
-    ssh match {
-      case None => if (root.is_dir) repository(root) else clone_repository(source, root)
-      case Some(session) =>
-        using(session.sftp())(sftp =>
-          if (sftp.is_dir(root)) repository(root, ssh = ssh)
-          else clone_repository(source, root, ssh = ssh))
-    }
+  {
+    val present =
+      ssh match {
+        case None => root.is_dir
+        case Some(session) => using(session.sftp())(_.is_dir(root))
+      }
+    if (present) { val hg = repository(root, ssh = ssh); hg.pull(); hg }
+    else clone_repository(source, root, options = "--noupdate", ssh = ssh)
+  }
 
   class Repository private[Mercurial](root_path: Path, ssh: Option[SSH.Session])
   {