summaryrefslogtreecommitdiff
path: root/src/reporting.mli
AgeCommit message (Collapse)Author
2018-10-31Rename Reporting_basic to ReportingAlasdair Armstrong
There is no Reporting_complex, so it's not clear what the basic is intended to signify anyway. Add a GitHub issue link to any err_unreachable errors (as they are all bugs)