mathlib
0578d23f - chore: update scripts/port_status for more flexible tagging (#17056)

Commit
3 years ago
chore: update scripts/port_status for more flexible tagging (#17056) In https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status we would like to be able to write more complicated statuses, like * `Yes mathlib4#999 1234abcd` to track commit information about the port * `No blocked by ring tactic` * `No PR'd as ...` This update to the script checks if the status starts with `Yes` or `No` to determine status. Further, when reporting good candidates for porting, it includes the comment after `No` if present. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading