Re: [sage-devel] help needed with git schlamassel

2017-09-19 Thread 'Martin R' via sage-devel
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

Re: [sage-devel] help needed with git schlamassel

2017-09-19 Thread Thierry
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

[sage-devel] help needed with git schlamassel

2017-09-19 Thread 'Martin R' via sage-devel
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.