diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-05 10:40:41 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-09 23:02:59 +0100 |
| commit | e5fbfbb162f95b30426fbe06f278c6d031abfd8a (patch) | |
| tree | f65c7f280019587d2c3f5a59ee6056e88b8c9ced /printing/prettyp.ml | |
| parent | 56ba2afe14a19bd0d396f89cab3ae720f2664be3 (diff) | |
[toplevel] Small refactoring of fatal_error functions.
Diffstat (limited to 'printing/prettyp.ml')
0 files changed, 0 insertions, 0 deletions