Merge branch 'feature/dune-exception-derived-from-std-exception' into 'master'

Feature/dune exception derived from std exception

I almost missed Christian's last commit. It was poor luck  that I had a look into the commit history before replacing the old remote URL by the new, Gitlab-based one. I manually transferred his commit and saved myself the work of programming what Christian already did.

See merge request !2