@Niklp09 as discussed: i force-pushed the master back to the previous commit, this here was the commit it pointed to before, not sure if you still need that, if not: feel free to close :+1:
Ah, btw, the procedure to force-push:
# checkout the commit you want `master` to point to
git checkout <commit-hash>
# set the master branch to it
git branch -f master
# check it out (i think it just sets the HEAD ref)
git checkout master
# push it to the remote
git push -f origin master
NOTE: only do this if the history hasn't propagated much (isn't been used anywhere) otherwise it could mess up update-scripts and things like that, a git revert would be the other option, but this just makes an additional commit with the reversed diff
Niklp09
commented
1 year ago
@Niklp09 as discussed: i force-pushed the master back to the previous commit, this here was the commit it pointed to before, not sure if you still need that, if not: feel free to close :+1:
Ah, btw, the procedure to force-push:
NOTE: only do this if the history hasn't propagated much (isn't been used anywhere) otherwise it could mess up update-scripts and things like that, a
git revertwould be the other option, but this just makes an additional commit with the reversed diff