src/Pure/General/mercurial.scala
changeset 73702 7202e12cb324
parent 73624 f033d4f661e9
child 75393 87ebf5a50283
equal deleted inserted replaced
73701:d83e7e444b43 73702:7202e12cb324
   374               else phabricator.create_repository(repos_name, short_name = repos_name)
   374               else phabricator.create_repository(repos_name, short_name = repos_name)
   375             }
   375             }
   376 
   376 
   377           while (repos.importing) {
   377           while (repos.importing) {
   378             progress.echo("Awaiting remote repository ...")
   378             progress.echo("Awaiting remote repository ...")
   379             Time.seconds(0.5).sleep
   379             Time.seconds(0.5).sleep()
   380             repos = phabricator.the_repository(repos.phid)
   380             repos = phabricator.the_repository(repos.phid)
   381           }
   381           }
   382 
   382 
   383           repos.ssh_url
   383           repos.ssh_url
   384 
   384