diff options
Diffstat (limited to 'tools/coq_tex.ml4')
| -rw-r--r-- | tools/coq_tex.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coq_tex.ml4 b/tools/coq_tex.ml4 index 1a9b9c73f..42d3f8f0a 100644 --- a/tools/coq_tex.ml4 +++ b/tools/coq_tex.ml4 @@ -122,7 +122,7 @@ let insert texfile coq_output result = let next_block k = if !last_read = "" then last_read := input_line c_coq; (* skip k prompts *) - for i = 1 to k do + for _i = 1 to k do last_read := remove_prompt !last_read; done; (* read and return the following lines until a prompt is found *) |