Invalid linked to issues and PRs after project changed hosting
I saw a link towards an issue involving me in a context that didn't make sense to me, which prompted me to discover this:
For example, if you look at a link named #49 that used to point at https://git.robur.coop/robur/miou/pulls/49 (a PR that adds a Miou.Lazy module), now it would point to #49 which is an issue that is unrelated discussing another topic.
I guess this is a minor issue, which only is encountered if someone tries following such links in comments, or from the changelog.
Not sure what could be done about this. Opening this issue to see if you are aware of that. Thanks!
Thank you for your report, I will try to find a solution. This is mainly due to the fact that the GitHub repository is a mirror of our repository on git.robur.coop. We will probably fix this issue by putting the real link to the PR (whether it comes from git.robur.coop or GitHub).
I just updated links and references into the CHANGES.md. The GitHub interface still can refer to bad PR/issue but I can not fix GitHub 🥲 .