reference manual after mathlib move

Stream: general

[Kevin Buzzard]

I don't really understand how all this project moving really works (mathlib moved to leanprover-community, and inspired by this Patrick moved the perfectoid project there too). It just occurred to me that perhaps the reference manual needed updating, because in section 1.4.3

https://leanprover.github.io/reference/using_lean.html#using-the-package-manager

it says

leanpkg new my_awesome_pkg
cd my_awesome_pkg
leanpkg add leanprover/mathlib
# shorthand for `leanpkg add https://github.com/leanprover/mathlib`

I thought "aah, this won't work now" -- but I just tried it, and it still seems to work fine. Will this stay working in the future? The leanpkg.toml generated by this still says mathlib = {git = "https://github.com/leanprover/mathlib", rev = "f529870e34eb5370ae8ac1f49f728547e4f6bbe5"} though. Is this OK?

[Johan Commelin]

Currently leanprover/mathlib is a link or forward or whatever to leanprover-community/mathlib. It does seem a good idea to update this documentation.