A follow-up merge-request to core/dune-grid!539 (merged)
Fine with me!
mentioned in commit bb492802
merged