author | wenzelm |
Fri, 21 Oct 2016 11:00:16 +0200 | |
changeset 64330 | d9a9ae3956f6 |
parent 64329 | 8f9d27c89241 |
child 64331 | abf7b6e6865f |
--- a/src/Pure/General/mercurial.scala Thu Oct 20 20:03:32 2016 +0200 +++ b/src/Pure/General/mercurial.scala Fri Oct 21 11:00:16 2016 +0200 @@ -25,6 +25,9 @@ /* repository access */ + def is_repository(root: Path, ssh: Option[SSH.Session] = None): Boolean = + new Repository(root, ssh).command("root").ok + def repository(root: Path, ssh: Option[SSH.Session] = None): Repository = { val hg = new Repository(root, ssh)