Merge branch 'develop' into 'master'

Develop

See merge request !103
4 jobs for master in 48 minutes and 21 seconds
latest
Status Job ID Name Coverage
  Test
passed #8833
debian:10 clang-6-libcpp-17

00:26:17

passed #8832
debian:10 gcc-8-17

00:17:56

passed #8834
debian:9 gcc-6-14

00:18:37

passed #8835
ubuntu:18.04 clang-6-17

00:24:02