diff options
| author | Pierre-Marie Pédrot | 2017-09-01 00:19:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-01 00:19:33 +0200 |
| commit | 2a0a48834f0b90319e56ae9f4a172fe6855583c0 (patch) | |
| tree | 10f7d831e2e2ef8923085f816f7431edf4cd1a7b /src | |
| parent | 72e3d2e563e08627559065ff0289403591d99682 (diff) | |
Passing an optional message to Tactic_failure.
Diffstat (limited to 'src')
0 files changed, 0 insertions, 0 deletions