Merge branch 'feature/make-version-check-of-suggested-module-non-fatal' into 'master' (!443) · Merge requests · Core Modules / dune-common · GitLab

Markus Blatt requested to merge cherry-pick-601c6f8e into releases/2.6 Jan 23, 2018

Make version check of suggested modules non-fatal.

See merge request !433 (merged)

(cherry picked from commit 601c6f8e)

735dc88a Make version check of suggested modules non-fatal.