diff options
| author | Robert Norton | 2017-03-10 10:49:52 +0000 |
|---|---|---|
| committer | Robert Norton | 2017-03-24 16:46:31 +0000 |
| commit | c10f2738f14c1f0aa60c18b01119d544140905b5 (patch) | |
| tree | 5c7409b5a757c4a8df9df539ab6c060cb97a425d /src/reporting_basic.ml | |
| parent | dee8e5c004bc3eb13a6470f3e3c5947ca7d2be64 (diff) | |
Minor cleanup: remove unnecessary brances and use 'not' iso ~.
Diffstat (limited to 'src/reporting_basic.ml')
0 files changed, 0 insertions, 0 deletions