diff options
| author | Peter Sewell | 2017-02-13 17:30:44 +0000 |
|---|---|---|
| committer | Peter Sewell | 2017-02-13 17:30:44 +0000 |
| commit | 352d86f08d2f18651eeeccdbedb0ff359e312e37 (patch) | |
| tree | 10078af4daa2675058e338228817e7f9758345f2 /src/reporting_basic.mli | |
| parent | 0f5eb59075c832fc69d32a9cdf5c417032f2bf9c (diff) | |
make syntax typeset in manual in ASCII-friendly style rather than using
math symbols. This breaks the l2.pdf build in language/ (for the moment).
Diffstat (limited to 'src/reporting_basic.mli')
0 files changed, 0 insertions, 0 deletions