23 Nov
2020
23 Nov
'20
3:04 p.m.
Hi, We are planning a move of the git server on Nov 23th at 20 UTC. There will be a DNS switch and some quick tweaks that will be needed after it. Expect a bit of downtime during the intervention. Use the gitlab or github mirror if you really need to access/clone it. Cheers, Jonathan