On 8/22/2022 5:01 PM, Segher Boessenkool wrote:
Hi!
On Mon, Aug 22, 2022 at 09:48:01PM +0200, Andrea Bocci wrote:
For the avoidance of doubt, "PR" in this context means "problem report"
i.e. bug report, not "pull request".
Yeah, sorry for the confusion. We talk about PRs in GCC a lot, since
time immemorial, long before github existed anyway. We do not use
github's workflows, they are not suitable for us.
Likely goes all the way back to the days when we used PRMS/GNATS for bug
tracking, so probably 25 years.
jeff
