Skip to content

Merge branch 'fix/deprecationwarnign-dune29' into 'master'

Timo Koch requested to merge cherry-pick-d2f7d2c9 into releases/3.6

Remove deprecation warnings with dune 2.9

See merge request !133 (merged)

(cherry picked from commit d2f7d2c9)

6cd49d4a Remove deprecation warnings with dune 2.9

Merge request reports