Apply 1 suggestion(s) to 1 file(s)
Passed
Robbert Krebbers
created pipeline for commit
6a49c6dd
, finished
Related merge request !484 to merge fin-notations
13 minutes 17 seconds, queued for 3 seconds