Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
They're just painful to have. It's not a number of an issue we're resolving because a PR can resolve more than one. So it had to be a PR id, but that's a bit chicken-and-eggy. Moreover, the “–“ in there is currently a non-ascii symbol, which can again be painful in some cases. So just remove the numbers for now, maybe we'll change it later.
- Loading branch information