mathlib3
1507ed4a - feat(scripts/port_status): output `git diff` command (#17630)

Commit
3 years ago
feat(scripts/port_status): output `git diff` command (#17630) We modify the `port_status` script to instead of listing files that have been modified, outputting the `git diff` command required to see the file at the current moment vs the commit that it is officially ported towards. Co-authored-by: Eric Rodriguez <ericrboidi@gmail.com>
Author
Parents
Loading