diff options
Diffstat (limited to 'tools/coq-tex.ml4')
-rw-r--r-- | tools/coq-tex.ml4 | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/tools/coq-tex.ml4 b/tools/coq-tex.ml4 index 5f42c03b0..d9b2ff2be 100644 --- a/tools/coq-tex.ml4 +++ b/tools/coq-tex.ml4 @@ -64,6 +64,8 @@ let extract texfile inputv = outside () in try + output_string chan_out + ("Set Printing Width " ^ (string_of_int !linelen) ^".\n"); outside () with End_of_file -> begin close_in chan_in; close_out chan_out end @@ -205,6 +207,7 @@ let insert texfile coq_output result = in try let _ = next_block 0 in (* to skip the Coq banner *) + let _ = next_block 0 in (* to skip the Coq answer to Set Printing Width *) outside () with End_of_file -> begin close_in c_tex; |