Closed github-actions[bot] closed 1 year ago
I notice with these you're merging then deleting the branch, is that a necessary manual deletion @Remi-Gau?
is that a necessary manual deletion
nope: I don't think that leaving the branch will interfere with anything (like a follow up automated PR). Mostly my OCD kicking in.
done via this GitHub Action