Fixed #1724 -- Renamed "patch" to "pull request"

[bmispelon]

This follows Django ticket # 35894

[bmispelon]

@sarahboyce Are you OK with those new names?

• Patches ➡️ Pull requests (category title)
• Patches needing review ➡️ PRs needing review
• Doc. patches needing review ➡️ Doc. PRs needing review

Here is how it looks like:

[sarahboyce]

Patches ➡️ Pull requests (category title)

Yes, but can we move "Easy ticket" somewhere else? Maybe into "Accepted tickets by type"?

Patches needing review ➡️ PRs needing review
Doc. patches needing review ➡️ Doc. PRs needing review

Wordy but "Tickets with PRs needing review" would be more accurate (and "Doc. tickets with PRs needing review")

[bmispelon]

Yes, but can we move "Easy ticket" somewhere else? Maybe into "Accepted tickets by type"?

Good idea, added 👍🏻 (this is something that can be done via the admin by the way)

Wordy but "Tickets with PRs needing review" would be more accurate (and "Doc. tickets with PRs needing review")

It does stretch the boxes a little bit, but I don't think it's so bad:

[sarahboyce]

I don't mind the stretch at all 😁
"PRs to review with tickets" and "Ticketed PRs to review" is the shortest I can think of if we want to make them shorter (but saves only a handful of characters)

[bmispelon]

I don't mind the stretch at all 😁 "PRs to review with tickets" and "Ticketed PRs to review" is the shortest I can think of if we want to make them shorter (but saves only a handful of characters)

You look at the dashboard more than me (not a high bar 😁 ), so I defer to your opinion on this.

[sarahboyce]

@nessita are you happy with the naming below?