Other than flagging certain commits as suggested in #18 "Check for non-gccrs things in the commits we cherry-pick", does gerris (intend to) have a mechanism for skipping arbitrary commits, for example by path matching (for .github/[...] etc. files), and/or by putting a marker into the Git commit log or similar (for commits that are local-only for other reasons)?
Other than flagging certain commits as suggested in #18 "Check for non-gccrs things in the commits we cherry-pick", does gerris (intend to) have a mechanism for skipping arbitrary commits, for example by path matching (for
.github/[...]etc. files), and/or by putting a marker into the Git commit log or similar (for commits that are local-only for other reasons)?