Small bug fixes, including for #122
Failed
robinwilliam.hundt
created pipeline for commit
4991cd34
, finished
1 related merge request: !120 Bug fixes
4 minutes 44 seconds, queued for 3 seconds