27.12.2023 12:21, Philippe Mathieu-Daudé wrote:
..
A more useful use of our time would be a git pre-merge hook on
our CI, but that won't work because PR aren't merged on the CI
but externally, and the final commit is pushed.
The only place I can think of to automate that is to have a
script on the maintainer side. Remembering Peter had a such
script, I found a reference in the list:
https://git.linaro.org/people/pmaydell/misc-scripts.git/commit/?id=f9a317392e8
Stefan, do you mind using Peter's script for your merges?
Similar script (to check for things like that which are
absolutely unacceptable) can be used as a commit hook on
gitlab repo for staging branch.
/mjt
