summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorPeter Sewell2017-02-13 17:30:44 +0000
committerPeter Sewell2017-02-13 17:30:44 +0000
commit352d86f08d2f18651eeeccdbedb0ff359e312e37 (patch)
tree10078af4daa2675058e338228817e7f9758345f2 /src
parent0f5eb59075c832fc69d32a9cdf5c417032f2bf9c (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')
0 files changed, 0 insertions, 0 deletions