Merge pull request #7 from gjaeger/develop

 Merge remote-tracking 'gitlab/develop' into github/develop
2 jobs for develop in 33 seconds (queued for 2 seconds)
latest
Status Job ID Name Coverage
  Configure
passed #110080
linux
configure-linux

00:00:03

 
  Compile
passed #110081
linux
make-linux

00:00:30