Merge branch 'cherry-pick-4455a367' into 'releases/3.4'

Merge branch 'bernd-master-patch-25084' into 'master'

See merge request !2763
6 jobs for releases/3.4 in 0 seconds (queued for 58 minutes and 30 seconds)
Status Name Job ID Coverage
  Trigger
canceled full-dune-2.7-clang

failed full-dune-2.7-gcc

canceled full-dune-master-clang

failed full-dune-master-gcc

passed minimal-dune-2.7-gcc

 
  Downstream Modules
canceled trigger lecture