diff options
| author | Peter Sewell | 2017-01-30 10:29:35 +0000 |
|---|---|---|
| committer | Peter Sewell | 2017-01-30 10:29:35 +0000 |
| commit | 54d1aa1493c9e058fc765a3c812da85ca3330693 (patch) | |
| tree | 3cda2a8e4e9ff749f1e27ecc3365960442190efa /src/reporting_basic.ml | |
| parent | 0189ef186771a7f5ea40a750dc0b9922ff8adbf5 (diff) | |
remove "rm *.tex" from language/Makefile "make clean"
Diffstat (limited to 'src/reporting_basic.ml')
0 files changed, 0 insertions, 0 deletions