Heads up: Lake changes in latest nightly

Stream: lean4

[Gabriel Ebner]

The latest Lean 4 nightly that was released -30 minutes ago comes with a new Lake version, which moved around the manifest location and the directory that dependencies are fetched into. Please keep that in mind when upgrading, you should probably change the .gitignore file.

[Jireh Loreaux]

Sorry, what exactly needs to be done? Surely we don't add lean_packages/manifest.json to the .gitignore? I'm not familiar with the details of the way lake works yet.

[Gabriel Ebner]

You can look at mathlib4#720 for inspiration. You need to change the .gitignore file and don't forget to add the lake-manifest.json file!

[Jannis Limperg]

This is a very nice change, thanks!