diff options
| author | Philipp Gesang <phg@phi-gamma.net> | 2018-07-21 14:10:13 +0200 |
|---|---|---|
| committer | Philipp Gesang <phg@phi-gamma.net> | 2018-07-21 14:10:13 +0200 |
| commit | 6a3b7da6a16a9d3a1f8ea3705d019ef5181ef2e5 (patch) | |
| tree | c7687c61645daa6f4b4e10bb34ebf7ddad72ead2 | |
| parent | 1f06b86a7aee14341c47377cedf2153e1405c02c (diff) | |
| download | context-mirror-bot-6a3b7da6a16a9d3a1f8ea3705d019ef5181ef2e5.tar.gz | |
add Aditya’s github repo
| -rw-r--r-- | context_mirror_bot.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/context_mirror_bot.ml b/context_mirror_bot.ml index 61d3535..2ac9d97 100644 --- a/context_mirror_bot.ml +++ b/context_mirror_bot.ml @@ -21,7 +21,7 @@ ****************************************************************************** * * Contact: Philipp Gesang <phg@phi-gamma.net> - * Repo: https://gitlab.com/phgsng/context-mirror + * Repo: https://gitlab.com/phgsng/context-mirror-bot * *****************************************************************************) @@ -64,8 +64,9 @@ 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" , "git@bb-git-mirror:phg/context-mirror.git" (* our old mirror *) + ; "new" , "git@gitlab.com:phgsng/context-mirror.git" (* our current mirror *) + ; "ghub", "git@github.com:contextgarden/context-mirror.git" ] (* github mirror *) let sources = [ { name = "beta"; @@ -77,10 +78,9 @@ let sources = (* owner and contact details for the user agent string *) let bot_owner = "Philipp Gesang" -let owner_contact = "phg@phi-gamma.net" +let owner_contact = "phg+robots@phi-gamma.net" -(*let repo_root = "/home/mirror/mirror"*) -let repo_root = "/home/phg/src/context-mirror" +let repo_root = "/home/mirror/mirror" let repo_subdir = "context-git" let repo_dir = Filename.concat repo_root repo_subdir let git_dir = Filename.concat repo_dir ".git" |