release notes typo

Stream: lean4

[Patrick Massot]

I was browsing https://github.com/leanprover/lean4/blob/releases/v4.8.0/RELEASES.md, hoping to find explanations about lake breaking changes since 4.8.0-rc1. I didn’t find what I was looking for but I notice a PR number issue. The line about “enables import auto-completions.” does not have the right PR number.

[Kyle Miller]

Oops, that should be lean4#3602

[Utensil Song]

image.png

Another one. And the one below is actually a feature or a fix IIUC.

[Kim Morrison]

Fixed, thanks.

[Utensil Song]

image.png

Ah, reading the description of lean#3601 makes me realized that this is indeed a breaking change, yet mitigate-able if one really wishes to run it without lake exe. It would be nice to have issue/PR numbers on the breaking changes, but all of them don't have the numbers, so one will need to search based on text.