clarified setup_repository: more uniform pull vs. clone, without update;
--- 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(
--- 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])
{