diff options
| author | Guillaume Melquiond | 2015-07-29 19:58:39 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-07-29 19:58:39 +0200 |
| commit | 9a5fb78ef3c7c5d4f568a4d04e169475e9105def (patch) | |
| tree | 0faa6e34dab303a0b0306cef94600a3ec2f3184d /dev | |
| parent | ffb2788b92323901c1024d1eae221e4beb4b6670 (diff) | |
Make coq-tex more robust with respect to the (non-)command on the last line.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions