aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Configuration.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-03-16 12:23:29 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2015-03-16 12:23:29 +0100
commitb3c67667b7121b7f2e50700ec6da4bd780dee426 (patch)
treefbd6cfe3b6cfda555ca9389e58a2b226df480013 /driver/Configuration.ml
parenta84576b219c797467e480508fc99ba78260062df (diff)
downloadcompcert-kvx-b3c67667b7121b7f2e50700ec6da4bd780dee426.tar.gz
compcert-kvx-b3c67667b7121b7f2e50700ec6da4bd780dee426.zip
Started implementing the printing functions for the debug info. Added a global target dependend option to activate the printing only for targets wher it works.
Diffstat (limited to 'driver/Configuration.ml')
-rw-r--r--driver/Configuration.ml6
1 files changed, 6 insertions, 0 deletions
diff --git a/driver/Configuration.ml b/driver/Configuration.ml
index 0012dc0c..48c31767 100644
--- a/driver/Configuration.ml
+++ b/driver/Configuration.ml
@@ -93,4 +93,10 @@ let asm_supports_cfi =
| "false" -> false
| v -> bad_config "asm_supports_cfi" [v]
+let advanced_debug =
+ match get_config_string "advanced_debug" with
+ | "true" -> true
+ | "false" -> false
+ | v -> bad_config "advanced_debug" [v]
+
let version = get_config_string "version"