Closed neeasade closed 3 years ago
Accident: the github default is currently squash and merge, but that's not what we want for upstream pulls (want to preserve the commits).
need for force push a revert, or revert and redo the PR
better revert instead of forcepush, because a lot of people building downstream distro packages from it
cf https://git.suckless.org/st/log.html