From 65fe9e7a4184003d64a131a93e28461dce82568e Mon Sep 17 00:00:00 2001 From: Philipp Gesang Date: Wed, 5 Feb 2020 01:14:40 +0100 Subject: set mirror user for Gitlab --- context_mirror_bot.ml | 4 ++-- 1 file 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 = -- cgit v1.2.3