Re: Implements DOM-id property for grobs. (issue 5504106)

[David Kastrup]

"address@hidden" <address@hidden> writes:

> I also fixed this in the reverted patch.  Unfortunately, I did not
> save the final pushed version of the patch - do you have a copy of it?
> If so, I won't need to make the changes again.

Unless you scrapped your whole repository,

git cherry-pick 6abea44be29f2de2abbc840507c9184132c8024d

should revive that patch as the last commit, and you can then work with
git commit --amend for changing parts of it.

In case you need to revive stuff that is no longer in any branch
git reflog
will almost always help.

Git starts garbage collecting inaccessible commits after about 3 months
by default.  Plenty of time to get them back if one really messed up.

-- 
David Kastrup