diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-05-26 02:35:24 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-05-26 02:35:24 +0200 |
| commit | 715388a4796aedb82cd6c7d5f51a21e3d655db4f (patch) | |
| tree | 75019f7e9dffa249538ab968bde6546f4e3e0556 /checker/votour.ml | |
| parent | 9c8cdd5f6c1cb4bda2f8558c17df3ffe69c49264 (diff) | |
[votour] Fix build with -safe-string (bug 5553)
Diffstat (limited to 'checker/votour.ml')
| -rw-r--r-- | checker/votour.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/checker/votour.ml b/checker/votour.ml index 48f9f45e7..44ca8ef31 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -313,8 +313,7 @@ let dummy_header = { } let parse_header chan = - let magic = String.create 4 in - let () = for i = 0 to 3 do magic.[i] <- input_char chan done in + let magic = really_input_string chan 4 in let length = input_binary_int chan in let objects = input_binary_int chan in let size32 = input_binary_int chan in |