Skip to content

Change name of exported type

Sander, Oliver requested to merge further-ci-fixes into master

The current test in dune-tnnmg now wants 'Vector' instead of 'VectorType'.

Merge request reports