lake update not pointing to custom fork

Stream: lean4

[Thomas Murrills]

In the mathlib branch lean-pr-testing-2679 (#7686), I need to point to a custom fork of std4 to adapt to the changes of the lean4 PR in question. However, when I run lake update, it generates a manifest which apparently points to leanprover/std4:main. Am I reading the manifest correctly? If so, can anyone else reproduce?

[Scott Morrison]

@Thomas Murrills, no, for me either lake update or lake update std in that branch results in a lake-manifest.json with std pointing at lean4-2679.

[Scott Morrison]

(Separately, I know this is all still undocumented, but you will make my life epsilon easier if the std branches also follow the naming scheme lean-pr-testing-2679.)

[Thomas Murrills]

Hmm, strange. I wonder what could be up with my setup!

Also, noted; will do. :)

[Joachim Breitner]

Did you try deleting lakefile.olean?