I'm not sure if I've got the house rule right, but I thought it's more that a core dev needs to repeat the bootstrap and verify that the binary in the GPR is the same (@xavierleroy?)

In this case, the GPR needs to be rebased in order to be mergeable - so the GPR author would have had to rebase the PR, redoing the bootstraps and then a core dev would have needed to re-do the re-done bootstraps to check that they are the same. Seems a bit inefficient.

@nojb, thanks for the rebase. Unfortunately, it needs to be rebased again.

Thanks, will update shortly.

Rebased. I will merge by end-of-day unless someone speaks up.

Is it end-of-day already ? :)

Yes, will merge as soon as the CI is green. Sorry for the wait, but I had to rebase once again due to some recently merged PR.

Merged, thank you!