diff options
| author | Pierre-Marie Pédrot | 2020-12-11 17:55:49 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-12-11 17:55:49 +0100 |
| commit | 7615b53cbcee95677996d60eb1c5ecc667559759 (patch) | |
| tree | 66e90bc5e9e1fbe7c28d3312e4295bf3195b16ff /dev/ci | |
| parent | c8d2248cbbe2c713605e0c61d7342fad948072da (diff) | |
Use a registered printer for tactic coercion failure.
Otherwise we pay a high cost for printing that might never make it to
the user.
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions