Merge branch 'bugfix/dune-version-newer' into 'master'
[bugfix] correct DUNE_VERSION_NEWER alias
See merge request !353 (merged)
(cherry picked from commit 62714041)
6cc426ab [bugfix] correct DUNE_VERSION_NEWER alias
[bugfix] correct DUNE_VERSION_NEWER alias
See merge request !353 (merged)
(cherry picked from commit 62714041)
6cc426ab [bugfix] correct DUNE_VERSION_NEWER alias