diff options
| author | Alasdair Armstrong | 2018-12-20 22:58:44 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-12-20 23:07:24 +0000 |
| commit | 367f72900fd24bf51b135f04f6fd301f3e8efb15 (patch) | |
| tree | 782515d2b9dfda003ccab35b938d0cf3cf4028eb /src/error_format.ml | |
| parent | 0a9200153430f5e727b3ebe1fa272d4842069530 (diff) | |
Make sure sail -v prints useful version info
Diffstat (limited to 'src/error_format.ml')
0 files changed, 0 insertions, 0 deletions