diff options
Diffstat (limited to 'context_mirror_bot.ml')
| -rw-r--r-- | context_mirror_bot.ml | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/context_mirror_bot.ml b/context_mirror_bot.ml index 3475a76..8cfce96 100644 --- a/context_mirror_bot.ml +++ b/context_mirror_bot.ml @@ -68,13 +68,10 @@ let mirror_repos = [ "old" , "hg@bitbucket.org:phg/context-mirror.git" ; "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 = +let sources = (* No “current” anymore as of February 2020. *) [ { name = "beta"; - page = "http://www.pragma-ade.nl/download-2.htm"; - url = "http://www.pragma-ade.nl/context/beta/cont-tmf.zip"; }; - { name = "current"; page = "http://www.pragma-ade.nl/download-1.htm"; - url = "http://www.pragma-ade.nl/context/current/cont-tmf.zip"; } ] + url = "http://www.pragma-ade.nl/context/latest/cont-tmf.zip"; } ] (* owner and contact details for the user agent string *) let bot_owner = "Philipp Gesang" |