Closed sjaeckel closed 2 years ago
Whatever I did on this PR, it somehow lost the diff of the 4 commits ...
Whatever I did on this PR, it somehow lost the diff of the 4 commits ...
That's really curious! I'm interested what happened here 🤔 Never seen this behaviour before.
I think I remember what went wrong ...
I merged locally, then couldn't push because @pasis added another commit on remote/master. So I rebased master on top of remote/master and pushed this one. (I guess that's where it went wrong)
Then I realized that I didn't update this branch, so I reset the branch head to the same commit as master and force-pushed this branch. But because the commits were already on master there was no diff anymore ...
Some house-keeping and minor features I stumbled over while looking through the code.