aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Configuration.ml
diff options
context:
space:
mode:
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"