Wolfgang Walther a705a34a22 ci/github-script/labels: prevent closing purposely-empty PRs ...

Some PRs are empty on purpose, for example the yearly notification about
the election for voters. We should not close these because the merge
commit is empty - only if there was a change intended, but the merge
commit *becomes* empty, we should act.

2025-10-19 11:27:05 +02:00

18 KiB

Raw Blame History

View Raw