summaryrefslogtreecommitdiff
path: root/checklink/Library.ml
diff options
context:
space:
mode:
authorGravatar varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-06-01 15:20:35 +0000
committerGravatar varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-06-01 15:20:35 +0000
commitd4b3174fb44f4c790c258932f8f4d27ad73aefd7 (patch)
tree4e72005304d97d3ef19697425dc9c4845f3931d6 /checklink/Library.ml
parent20d10f71ea444e326a7a77670844214375c72514 (diff)
checklink: improved error messages
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1909 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'checklink/Library.ml')
-rw-r--r--checklink/Library.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/checklink/Library.ml b/checklink/Library.ml
index 0ce3bcd..ebcbac8 100644
--- a/checklink/Library.ml
+++ b/checklink/Library.ml
@@ -140,6 +140,7 @@ let string_of_bitstring bs =
(* To print addresses/offsets *)
let string_of_int32 = Printf.sprintf "0x%08lx"
+let string_of_int64 = Printf.sprintf "0x%08Lx"
(* To print counts/indices *)
let string_of_int32i = Int32.to_string