Merge branch 'robbert/map_filter' into 'master'
Passed
Robbert Krebbers
created pipeline for commit
f53dfb6d
, finished
For master
9 minutes 49 seconds, queued for 2 seconds