aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/votour.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/votour.ml')
-rw-r--r--checker/votour.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/votour.ml b/checker/votour.ml
index afc1c17a9..11b95c93c 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -135,7 +135,7 @@ let visit_vo f =
let ch = open_in_bin f in
let _magic = input_binary_int ch in
let lib = (input_value ch : Obj.t) in (* actually Cic.library_disk *)
- let _ = (input_value ch : Digest.t) in
+ let _ = Digest.input ch in
let tbl = (input_value ch : Obj.t) in (* actually Cic.opaque_table *)
let () = close_in ch in
let o = if !opaque then tbl else lib in