Ralf's comments.
Passed
Robbert Krebbers
created pipeline for commit
9d444a80
, finished
Related merge request !461 to merge robbert/new_gmap
4 minutes 24 seconds, queued for 3 seconds