Commit 75fd4b6d authored by Oliver Sander's avatar Oliver Sander

Merge branch 'remove-unused-stuff' into 'master'

Remove unused stuff

See merge request staging/dune-functions!268
parents 4baee24b ea3be92f
Pipeline #30130 passed with stage
in 23 minutes and 29 seconds