Commit 03cdeb08 authored Jan 04, 2021 by Andreas Klöckner

Merge branch 'inducer-master-patch-95454' into 'master'

Shorten, standardize doc/conf

See merge request !13