diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-07-29 19:58:39 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-07-29 19:58:39 +0200 |
| commit | 9a5fb78ef3c7c5d4f568a4d04e169475e9105def (patch) | |
| tree | 0faa6e34dab303a0b0306cef94600a3ec2f3184d /tools | |
| parent | ffb2788b92323901c1024d1eae221e4beb4b6670 (diff) | |
Make coq-tex more robust with respect to the (non-)command on the last line.
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_tex.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml index 9c91889a0..f65708698 100644 --- a/tools/coq_tex.ml +++ b/tools/coq_tex.ml @@ -55,7 +55,10 @@ let extract texfile inputv = ("Set Printing Width " ^ (string_of_int !linelen) ^".\n"); outside () with End_of_file -> - begin close_in chan_in; close_out chan_out end + (* a dummy command, just in case the last line was a comment *) + output_string chan_out "Set Printing Width 78.\n"; + close_in chan_in; + close_out chan_out (* Second pass: insert the answers of Coq from [coq_output] into the * TeX file [texfile]. The result goes in file [result]. *) |