Merge branch 'develop' into 'master'

misc

See merge request !23
2 jobs for master in 3 minutes and 55 seconds (queued for 2 seconds)
Status Name Job ID Coverage
  Linux
passed githubjob #1086341

00:00:37

passed masterJobLinux #1086342

00:03:54