OK, I tried - I got this from two sources, so I took a chance, yes it did -
relief - thank you!
Martin
Am Mittwoch, 20. September 2017 07:31:54 UTC+2 schrieb Thierry
(sage-googlesucks@xxx):
>
> Hi,
>
> does 'git trac push --force' work ?
>
> Ciao,
> Thierry
>
>
>
> On Tue, Sep 19, 2017 at 10
Hi,
does 'git trac push --force' work ?
Ciao,
Thierry
On Tue, Sep 19, 2017 at 10:19:09PM -0700, 'Martin R' via sage-devel wrote:
> Dear git gurus,
>
> I accidentally pushed a merge to https://trac.sagemath.org/ticket/22921.
> Locally, I can "undo" this with
>
> git reset --hard 84093c4bc19
Dear git gurus,
I accidentally pushed a merge to https://trac.sagemath.org/ticket/22921.
Locally, I can "undo" this with
git reset --hard 84093c4bc19d2aa7e353dfa2b2436a5bf56b96b8
but I do now know how to do this on the ticket, and I am afraid of
following advice of some random git blog page.