git help

Stream: general

[Scott Morrison]

Sorry to have to ask about mundane things like how to use git, but... Say that I've got a fork of mathlib that is borked in some way (in my case, I merged in a commit from master, that Mario shortly thereafter deleted, but I have a branch that includes it).

Should I:
1) Just delete my whole fork (this is a good moment to do so, I have only two modified files).
2) Learn about ... rebasing? something else? Is it possible to actually get my master branch back to matching the main repository's master branch?

[Sebastian Ullrich]

Is it possible to actually get my master branch back to matching the main repository's master branch?

git reset --hard origin/master

[Scott Morrison]

But what about all the pushed commits to master on my github fork?

[Scott Morrison]

That won't bring my fork hosted on github back to matching the corresponding branch on the main github repo, will it?

[Sebastian Ullrich]

Ah. It will after a git push --force <your remote>.

[Scott Morrison]

But ... don't I have to strip commits or something?

[Scott Morrison]

I want my master branch in my fork to really look (history and everything) just like the master branch in origin.

[Scott Morrison]

Or is it okay to just continue on with my fork having its own alternative borked history?

[Sebastian Ullrich]

After these two commands, your fork's master will look exactly like the one in origin

[Scott Morrison]

Ah, and the --hard you added above means I don't even need to git checkout -- .. Thanks.

[Scott Morrison]

Wow, amazing! Everything is beautiful. :-)

[Sebastian Ullrich]

:)