Patchbot applies unwanted patches

[vbraun]

The patchbot is hoarding patches, it seems impossible to make him not apply a patch that occurs somewhere in the ticket. For example, see #12533. The final result of that ticket is just a single patch but the patchbot still wants to apply old patches.

In the case where the ticket description explicitly says "apply <file.patch>" I think the patchbot should simply ignore all comments and further attached patches.

CC: @robertwb

Component: packages: optional

Issue created by migration from https://trac.sagemath.org/ticket/13560

[robertwb]

comment:1

If I don't get around to it, pull requests can be sent to https://github.com/robertwb/sage-patchbot/

[fchapoton]

comment:4

Since we have switched to git, this can be closed.