Use `!` instead of `+`.
Passed
Robbert Krebbers
created pipeline for commit
b48d40e9
, finished
Related merge request !271 to merge robbert/hintmode
4 minutes 50 seconds, queued for 3 seconds