diff options
| author | Philipp Gesang <phg@phi-gamma.net> | 2020-02-05 01:14:40 +0100 |
|---|---|---|
| committer | Philipp Gesang <phg@phi-gamma.net> | 2020-02-05 01:14:40 +0100 |
| commit | 65fe9e7a4184003d64a131a93e28461dce82568e (patch) | |
| tree | 873ad6b4d588eca61ef506e91dcad8386b16f662 | |
| parent | 6a3b7da6a16a9d3a1f8ea3705d019ef5181ef2e5 (diff) | |
| download | context-mirror-bot-65fe9e7a4184003d64a131a93e28461dce82568e.tar.gz | |
set mirror user for Gitlab
| -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 = |