diff options
| author | Jason Gross | 2019-10-25 15:28:37 -0400 |
|---|---|---|
| committer | Jason Gross | 2019-10-29 12:32:57 -0400 |
| commit | c59815c860a11948359e96ecc51d566bb5e5d8fb (patch) | |
| tree | bdd7e2d7dbcf38e6e2d27de71a3d94dc80f46347 /dev/tools/pre-commit | |
| parent | e9dddcb2b5297f2e601a2e2d65a131ee5fde19e4 (diff) | |
`assert_succeeds`&`assert_fails`: multisuccess fix
These tactics now work correctly with multisuccess tactics by wrapping
the tactic argument in `once`.
Fixes #10965
Diffstat (limited to 'dev/tools/pre-commit')
0 files changed, 0 insertions, 0 deletions