fatal: ambiguous argument 'mathlib4#771..HEAD'

Stream: mathlib4

[Kevin Buzzard]

Is this happening for other people too:

~/lean-projects/mathlib$ ./scripts/port_status.py
fatal: ambiguous argument 'mathlib4#771..HEAD': unknown revision or path not in the working tree.
Use '--' to separate paths from revisions, like this:
'git <command> [<revision>...] -- [<file>...]'
fatal: ambiguous argument 'mathlib4#763..HEAD': unknown revision or path not in the working tree.
Use '--' to separate paths from revisions, like this:
'git <command> [<revision>...] -- [<file>...]'
fatal: ambiguous argument 'mathlib4#762..HEAD': unknown revision or path not in the working tree.
Use '--' to separate paths from revisions, like this:
'git <command> [<revision>...] -- [<file>...]'
# The following files have all dependencies ported already, and should be ready to port:
# Earlier items in the list are required in more places in mathlib.
control.traversable.basic
algebra.hom.group    -- mathlib4#659 8c53048add6ffacdda0b36c4917bfe37e209b0ba
data.nat.basic    -- WIP mathlib4#729 71ca477041bcd6d7c745fe555dc49735c12944b7
control.applicative

[seems to work fine after the errors...]

[Scott Morrison]

Yes, it's malformed entries in the port-status wiki page. If you search for mathlib4#771 you'll find it still says "PR" in that line. (Or it did, until I fixed some a moment ago.)

[Eric Wieser]

I think if we merge #17620 we would end up with better behavior here when the file is malformed

[Scott Morrison]

Yes, lets. @Patrick Massot, could you do a release of mathlib-tools?

[Patrick Massot]

I released.