diff options
| author | Erik Martin-Dorel | 2016-09-18 17:02:10 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-09-19 21:02:25 +0200 |
| commit | c46981cfcdfe804178e1fe48a8489de6f7733c9c (patch) | |
| tree | 966c1614765a3f2b1fc4972eda30ded84eb2f958 /Makefile.dev | |
| parent | 2aaa58c22e37b05e3637ac7161bb464da7db054a (diff) | |
Fix typos in RefMan-uti.tex.
- Ensure "coq_makefile --help" is properly typeset with HeVeA/PdfLaTeX
- Replace 's with "s so they are typeset as true ASCII characters
- Add missing ; before closing brace.
Diffstat (limited to 'Makefile.dev')
0 files changed, 0 insertions, 0 deletions