summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPhilipp Gesang <phg@phi-gamma.net>2020-02-05 01:14:40 +0100
committerPhilipp Gesang <phg@phi-gamma.net>2020-02-05 01:14:40 +0100
commit65fe9e7a4184003d64a131a93e28461dce82568e (patch)
tree873ad6b4d588eca61ef506e91dcad8386b16f662
parent6a3b7da6a16a9d3a1f8ea3705d019ef5181ef2e5 (diff)
downloadcontext-mirror-bot-65fe9e7a4184003d64a131a93e28461dce82568e.tar.gz
set mirror user for Gitlab
-rw-r--r--context_mirror_bot.ml4
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 =