Fixing out of sync Interlisp.github.io fork

[pamoroso]

To keep my Interlisp.github.io fork synchronized with the original I use the Sync fork menu command on GitHub.

Today the fork was 2 commits ahead (already merged) and Sync fork provided two options, merging or removing the commits. I usually do the latter but today I picked the merge option, which resulted in the fork still being 2 commits ahead. Moreover, creating a PR included those commits.

In an attempt to bring the fork back in sync I submitted a dummy PR asking @stumbo to reject it, which he did, in the hope GitHub would give again the syncing option to remove the commits. But the fork is still 2 commits ahead and now creating a PR includes the commits and lists the dummy PR:

On GitHub I can't find any way of deleting or undoing the commits. How can I bring my fork back in sync?

[nbriggs]

Can you just delete the fork and re-fork it?

[pamoroso]

If I delete the fork GitHub deletes only my copy even if I'm a member of the Interlisp organization, right?

[masinter]

Right, deleting a fork doesn't affect the repo your fork was made from.

[pamoroso]

I deleted my fork and re-forked, now everything is fine again.

[MattHeffron]

@pamoroso OK to close this?

[pamoroso]

@MattHeffron Sure, I'm closing the discussion.