[dune-pdelab] [dune-pdelab-commit] [branch] dune-pdelab - 'master' updated

[Christian Engwer]

Hi Steffen,

> sorry, I fat-fingered a magit command and pushed this from my local feature branch directly to GitLab master…
> 
> If someone wants to discuss this in a little more detail, I can revert the commits and open a merge request. Just
> yell at me.

I'm fine with this. I'd like gitlab to block access to master (perhaps
with some special trick like for the white-space-hook), but in this
particular case I like the changes (well... it's what we discussed on
the phone).

The only thing I don't like that much is the naming, I actually like
"raw", because it says what it is. Not in every case the underlying
data structure is something you can nicely work with, thus it is not
always the  "native" interface, but sometimes really just the raaw
data.

But as we have the name now, we can also keep it.

Ciao
Christia