aboutsummaryrefslogtreecommitdiff
path: root/lib/objFile.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-07-16 15:26:59 +0200
committerEmilio Jesus Gallego Arias2020-07-16 15:26:59 +0200
commitf54bc666c62ad9a66067cb486816cdfc68c2946d (patch)
tree3e6b02e8874778411765c161384b2bf6dc25b12c /lib/objFile.ml
parent3eccf67b2e4aed36fc6935900167b19bcf6dffde (diff)
parente52f070515833634f7a52e3440be02229e71d4fb (diff)
Merge PR #12677: Fix #12513: coq no longer reports mismatched version numbers.
Reviewed-by: ejgallego Reviewed-by: gares
Diffstat (limited to 'lib/objFile.ml')
-rw-r--r--lib/objFile.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/objFile.ml b/lib/objFile.ml
index 96db51a010..26367aaffa 100644
--- a/lib/objFile.ml
+++ b/lib/objFile.ml
@@ -182,7 +182,7 @@ let open_in ~file =
let version = input_int32 ch in
let () =
if not (Int32.equal magic magic_number) then
- let e = { filename = file; actual = version; expected = magic_number } in
+ let e = { filename = file; actual = magic; expected = magic_number } in
raise (Bad_magic_number e)
in
let () =