mathlib3
2f7913bd - fix(ci/add_ported_warnings): use a version of the action that does not error (#17936)

Commit

3 years ago

fix(ci/add_ported_warnings): use a version of the action that does not error (#17936) See https://github.com/jitterbit/get-changed-files/issues/19#issuecomment-854657729 for details.

Author

eric-wieser

Parents

daf8adf1

mathlib3 2f7913bd - fix(ci/add_ported_warnings): use a version of the action that does not error (#17936)

mathlib3
2f7913bd - fix(ci/add_ported_warnings): use a version of the action that does not error (#17936)