After a bit more testing, I think the even better response is to git reset
--hard
16feb and push that change. One part of the git documentation suggests one, another part suggests the other. I'm not clear on what the
differences
are.
The problem is that when I do a git diff and git status to make sure of
what
I'm about to push, it looks right...but then again, it also did when I
messed
things up.
Any opinions?
Would we not lose the commits listed here, then? https://github.com/phpmyadmin/phpmyadmin/commits/master
Best, J.M.