[dune-pdelab] Small bug

[Christian Engwer]

On Wed, Jul 01, 2015 at 10:30:33AM +0200, Oliver Sander wrote:
> > 
> > Ah, but that’s wrong anyway ;-)
> > 
> > As an external user, you should just include <dune/pdelab/backend/istl.hh> and let that header take care of including
> > everything else. That should probably be changed in all of those backward compatibility headers…
> >
> 
> The merge request should hit your desk shortly.
> 
> It still does feel like a lot of clicks for a single commit, though.

I kind of agree with Oli, but...

There are a couple of command line tools out there to trigger a
merge-request. I intend to test the (not all, only until I'm
sattisfied).

If I can create a branch, push it and open a corresponding merge
request, I don't think it is such a big thing anymore. Still we have
to find a good way how to balance the amount of work for
contributors. On the other hand I think for non-developers, the
workflow is still simpler than opening a bug-report and uploading a
patch. Furthermore the discussion about parts of the patches are
simpler with gitlab.

Anyhow, let us collect experiences and discuss after the release.

Christian