You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
When dependent PRs are made, then the heuristic of "look at all the changed files and attach them to this PR" doesn't work, because a file in a PR will also be attached to all its dependencies. This line in the make_port_status.py script then just picks the first one, essentially at random:
When dependent PRs are made, then the heuristic of "look at all the changed files and attach them to this PR" doesn't work, because a file in a PR will also be attached to all its dependencies. This line in the
make_port_status.py
script then just picks the first one, essentially at random:https://github.com/leanprover-community/mathlib4/blob/7e974fd3806866272e9f6d9e44fa04c210a21f87/scripts/make_port_status.py#L164
This also means that some PRs won't appear on the dashboard at all, because their association gets overwritten by a PR that depends on them.
cc @rwbarton, @jcommelin; reported by @mattrobball who noted leanprover-community/mathlib4#2332 didn't appear on the dashboard at all.
The text was updated successfully, but these errors were encountered: