[Dune-devel] Accidental push to dune-common:master

[Christian Engwer]

Dear all,

> I just accidentally pushed what was supposed to be a merge request directly to the
> master branch of dune-common (sorry about that…).
> 
> But that got me thinking: Should we just disable direct pushes to the master branch
> in the core modules?

we discussed this a while ago and at that time the response was that
several people where afraid of the extra effort to push mini changes
(like fixing a doc typo) via a merge request. On the other hand I have
the impression that everybody got accustomed to the new workflow and
people are also opening merge requests for such small changes. Thus I
have the impression that time is ready to just disable direct pushes.

Christian