summaryrefslogtreecommitdiff
path: root/checklink/Frameworks.ml
diff options
context:
space:
mode:
authorGravatar varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-06-04 08:53:56 +0000
committerGravatar varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-06-04 08:53:56 +0000
commit6256626f743bfcdd488fa1ec9d086d14f11109b4 (patch)
tree732c489f836a3eddd2eebcf8f66aa080d0eb0ce7 /checklink/Frameworks.ml
parentd4b3174fb44f4c790c258932f8f4d27ad73aefd7 (diff)
checklink: improved user-friendliness
Command-line options have been renamed and reordered. Error messages verbosity is more fine-grained. Possibly spurious debug messages are more clearly separated from the actual conclusions of the process. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1913 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'checklink/Frameworks.ml')
-rw-r--r--checklink/Frameworks.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/checklink/Frameworks.ml b/checklink/Frameworks.ml
index 828299e..72b00b4 100644
--- a/checklink/Frameworks.ml
+++ b/checklink/Frameworks.ml
@@ -187,6 +187,8 @@ let string_of_log_entry show_debug entry =
let fatal s = failwith ((format_logtype "FATAL: ") ^ s)
+let verbose_elfmap = ref false
+
let string_of_byte_chunk_desc = function
| ELF_header -> "ELF header"
| ELF_progtab -> "ELF program header table"
@@ -202,4 +204,4 @@ let string_of_byte_chunk_desc = function
| Jumptable -> "Jump table"
| Float_literal(f) -> "Float literal: " ^ string_of_float f
| Padding -> "Padding"
-| Unknown(s) -> " ??? " ^ s
+| Unknown(s) -> "???" ^ (if !verbose_elfmap then s else "")