diff options
| author | Philipp Gesang <phg@phi-gamma.net> | 2020-02-05 01:32:21 +0100 |
|---|---|---|
| committer | Philipp Gesang <phg@phi-gamma.net> | 2020-02-05 01:32:21 +0100 |
| commit | 3dcd73d7129fa142701b3e0739d862a709a5b8fb (patch) | |
| tree | 01e347a4a4b7c6f79c1884fb7aa24c538ca45310 | |
| parent | 74dc634d93980cbc5f992ab0f70e48d0bbdab5bd (diff) | |
| parent | 65fe9e7a4184003d64a131a93e28461dce82568e (diff) | |
| download | context-mirror-bot-3dcd73d7129fa142701b3e0739d862a709a5b8fb.tar.gz | |
Merge remote-tracking branch 'mirror/master'
| -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 6a0fd05..3475a76 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 = |