summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--context_mirror_bot.ml7
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"