PSA: if you use #codeberg don't click the merge button on pull requests. don't use the web interface to merge pull requests!
https://codeberg.org/Codeberg/Community/issues/3278
current responses on that thread are giving the runaround; hopefully they will act on it. sometimes, when you click merge on pull requests on codeberg, the patches will actually not show up in your git history, even when the PR shows as merged. this happened to me twice recently.
the second time i noticed it, and i was able to pull from my repo, and find the exact commit ID from the merged patch, but it wasn't on any branch. detached HEAD. so i checked out that commit ID, created a branch locally, and merged back into my master.
for now, absent migration to another code hosting provider, i will download patches from PRs manually and merge them locally, before re-pushing.
see issue. i hope they fix it. the current response there accuses me of force pushing - i didn't.
was gonna stay quiet but that initial response there displeases me.
