Please update the github link to the idris homepage

[juhp]

Currently it points at https://idris-lang.org/

The correct working url is https://www.idris-lang.org/

[juhp]

I mean the link in the about section of https://github.com/idris-lang/Idris2

However I just noticed the same link appears at the beginning of the README as well, so that should be fixed too.

Alternatively a redirect could be setup perhaps?

[CodingCellist]

The issue is to do with the DNS records, not the URLs. Clearly Edwin and I didn't update the DNS entirely correctly when we migrated to GH Pages (see also #3715). I don't have access to the DNS records (those are still Edwin-only, since he owns the domain), but I will try to find some time this week to update the webpage repo based on dunhamsteve's comment from the previously mentioned PR.

[ysangkok]

@CodingCellist Was the website repo updated as you planned? Or are we blocked on @edwinb ?

[juhp]

I would say it is better to fix the broken links now (and then revert them later when dns is updated, if you really want to).
At least for the github project the "cost" is very low, I think.

[CodingCellist]

Edwin has just updated the DNS records, so fingers crossed this is resolved over the next 24-48 hours?

[CodingCellist]

@juhp @ysangkok are you now able to connect to both https://idris-lang.org and https://www.idris-lang.org without errors or warnings (c.f. idris-lang/idris-lang.github.io#20 (comment))?

[ysangkok]

Yes, I get the same addresses in the AAAA and A records for www.idris-lang.org and idris-lang.org (no www).