aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Configuration.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2016-02-25 23:20:51 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2016-02-25 23:20:51 +0100
commit91284897bbc029cacabc36aae024a86a248814ae (patch)
tree09ec6d4ce93d42d978ba5fc0e19e3ac20a1c4ed0 /driver/Configuration.ml
parent9e09561f54db459757446db52c01bf3d85bd8764 (diff)
downloadcompcert-kvx-91284897bbc029cacabc36aae024a86a248814ae.tar.gz
compcert-kvx-91284897bbc029cacabc36aae024a86a248814ae.zip
Split up tools and options.
Added additional configuration entries to seperate tools from options in the .ini files. Internally they are just concatenated in Configuration.ml which allows it to still use old .ini files.
Diffstat (limited to 'driver/Configuration.ml')
-rw-r--r--driver/Configuration.ml15
1 files changed, 12 insertions, 3 deletions
diff --git a/driver/Configuration.ml b/driver/Configuration.ml
index 3025391b..1914c1b3 100644
--- a/driver/Configuration.ml
+++ b/driver/Configuration.ml
@@ -103,9 +103,18 @@ let tool_absolute_path tools =
absolute_path ini_dir tool in
tool::args
-let prepro = tool_absolute_path (get_config_list "prepro")
-let asm = tool_absolute_path (get_config_list "asm")
-let linker = tool_absolute_path (get_config_list "linker")
+let opt_config_list key =
+ match Readconfig.key_val key with
+ | Some v -> v
+ | None -> []
+
+let prepro =
+ tool_absolute_path (get_config_list "prepro")@(opt_config_list "prepro_options")
+let asm =
+ tool_absolute_path (get_config_list "asm")@(opt_config_list "asm_options")
+let linker =
+ tool_absolute_path (get_config_list "linker")@(opt_config_list "linker_options")
+
let arch =
match get_config_string "arch" with
| "powerpc"|"arm"|"ia32" as a -> a