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. > Ah... thanks for the clarification. > That is definitely something I can do :-) :-) Thanks in advance! Segher
