diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-10 03:22:24 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-10 03:22:24 +0200 |
| commit | b89c8f3846e8254651dbcba262f83d3d1fe3adb6 (patch) | |
| tree | 637106259894dc99ae71a5e1edb938ba5dfc7f62 /tools/coqdep_common.mli | |
| parent | dffba98368b5b1156e1933dc7377317281c57491 (diff) | |
[toplevel] Print error header on fatal batch error.
Diffstat (limited to 'tools/coqdep_common.mli')
0 files changed, 0 insertions, 0 deletions