diff options
Diffstat (limited to 'plugins/xml/xml.ml4')
| -rw-r--r-- | plugins/xml/xml.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/xml/xml.ml4 b/plugins/xml/xml.ml4 index 8a4eb39a1..c2523755b 100644 --- a/plugins/xml/xml.ml4 +++ b/plugins/xml/xml.ml4 @@ -55,7 +55,7 @@ let pp_ch strm channel = pp_r m s | [< >] -> () and print_spaces m = - for i = 1 to m do fprint_string " " done + for _i = 1 to m do fprint_string " " done and fprint_string str = output_string channel str in |