diff options
Diffstat (limited to 'context_mirror_bot.ml')
| -rw-r--r-- | context_mirror_bot.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/context_mirror_bot.ml b/context_mirror_bot.ml index 2ac9d97..c4485b5 100644 --- a/context_mirror_bot.ml +++ b/context_mirror_bot.ml @@ -64,8 +64,8 @@ exception Prepare_failed of string let bootstrap_repo = "git@bitbucket.org:phg/context-mirror.git" (* our mirror *) let garden_repo = "http://git.contextgarden.net/context/context.git" (* official, but broken *) (*let mirror_repo = "git@bitbucket.org:phg/context-mirror.git" [> our mirror <]*) -let mirror_repos = [ "old" , "git@bb-git-mirror:phg/context-mirror.git" (* our old mirror *) - ; "new" , "git@gitlab.com:phgsng/context-mirror.git" (* our current mirror *) +let mirror_repos = [ "old" , "hg@bitbucket.org:phg/context-mirror.git" (* our old mirror *) + ; "new" , "git@gitlab.com:context-mirror-bot/context-mirror.git" (* our current mirror *) ; "ghub", "git@github.com:contextgarden/context-mirror.git" ] (* github mirror *) let sources = |