Zulip Chat Archive

Stream: mathlib4

Topic: Procedure for using `add_port_comments.py`

Arien Malec (Nov 23 2022 at 18:19):

  1. Should I document the requirement to install mathlibtools from Github in #port-guide?
  2. When I run add_port_comments.py I assume I should only PR comments for files that I've ported, right? (I get hits for lots of files).

Eric Wieser (Nov 23 2022 at 18:22):

You do not need to run that script any more

Eric Wieser (Nov 23 2022 at 18:24):

The PRs are created automatically, see #17686

Arien Malec (Nov 23 2022 at 19:00):

Cool -- I'll update #port-guide

Last updated: Dec 20 2023 at 11:08 UTC