Merge branch 'bugfix/DuneMPI-use-COMPILE_OPTIONS' into 'master'
DuneMPI: append flags to `COMPILE_OPTIONS` instead of `COMPILE_FLAGS`
See merge request !499
(cherry picked from commit 96ed065a)
4063acee DuneMPI: append flags to `COMPILE_OPTIONS` instead of `COMPILE_FLAGS`