diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-06-14 18:18:00 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-14 18:18:00 +0200 |
commit | 5f3954b8d919a8fd89ce2332261698f41bc33550 (patch) | |
tree | d4c7ada4f9e813bddaa3bb1d1e46658e345a774f /theories | |
parent | cb41d7b40c401c15e9cb66f508f89dbd1bdcdbff (diff) | |
parent | b89c8f3846e8254651dbcba262f83d3d1fe3adb6 (diff) |
Merge PR#758: [toplevel] Print error header on fatal batch error.
Diffstat (limited to 'theories')
0 files changed, 0 insertions, 0 deletions