Bugfix/remove core fixes
After finally a couple of merge requests has been folded into dune-common it should be possible to remove the core-fixes stuff.
Edited by Claus-Justus Heine
After finally a couple of merge requests has been folded into dune-common it should be possible to remove the core-fixes stuff.