diff options
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]. *) |