[GRASS-dev] git merge mess on master

[Markus Neteler]

On Tue, May 21, 2019 at 11:23 AM Bas Couwenberg <sebastic at xs4all.nl> wrote:
> On 2019-05-21 11:22, Markus Neteler wrote:
> > How to revert that? Of course someone had to run into this at some
> > point, so seems I "volunteered" to be the first :((
>
> rebase and force push.

Thanks - we investigated further with two local git gurus, it seems
that nothing happened and things are indeed ok.

Best
Markus