Bring master up to date, merge updated CI

added 8 commits

• d60137a0...bcd9800a - 7 commits from branch master
• 263237fa - Merge branch 'master' into 'docu-ci'

Compare with previous version

enabled an automatic merge when the pipeline for 263237fa succeeds

mentioned in commit 065a9db7

merged