src/Pure/General/mercurial.scala
changeset 66558 37b16f8af351
parent 66105 8889aad1ff92
child 66569 1a475e59c70f
equal deleted inserted replaced
66557:b17d41779768 66558:37b16f8af351
    27 
    27 
    28 
    28 
    29   /* repository access */
    29   /* repository access */
    30 
    30 
    31   def is_repository(root: Path, ssh: Option[SSH.Session] = None): Boolean =
    31   def is_repository(root: Path, ssh: Option[SSH.Session] = None): Boolean =
    32     new Repository(root, ssh).command("root").ok
    32   {
       
    33     val root_hg = root + Path.explode(".hg")
       
    34     val root_hg_present =
       
    35       ssh match {
       
    36         case None => root_hg.is_dir
       
    37         case Some(ssh) => ssh.is_dir(root_hg)
       
    38       }
       
    39     root_hg_present && new Repository(root, ssh).command("root").ok
       
    40   }
    33 
    41 
    34   def repository(root: Path, ssh: Option[SSH.Session] = None): Repository =
    42   def repository(root: Path, ssh: Option[SSH.Session] = None): Repository =
    35   {
    43   {
    36     val hg = new Repository(root, ssh)
    44     val hg = new Repository(root, ssh)
    37     hg.command("root").check
    45     hg.command("root").check