Do not make sealed definitions TC opaque.
Passed
Robbert Krebbers
created pipeline for commit
fa725d2e
, finished
For master
8 minutes 12 seconds, queued for 2 seconds