diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-02-29 16:17:01 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-02-29 16:17:01 +0100 |
| commit | d8740a489984f63864a8e4ff728fb7f3871ecb34 (patch) | |
| tree | 6e616af57b82d64c54c7fc1d116aced42b9a2a6a /driver | |
| parent | 214fc8b834760925e77e3c713c1e7dcf06a4889e (diff) | |
| parent | 91284897bbc029cacabc36aae024a86a248814ae (diff) | |
| download | compcert-d8740a489984f63864a8e4ff728fb7f3871ecb34.tar.gz compcert-d8740a489984f63864a8e4ff728fb7f3871ecb34.zip | |
Merge remote-tracking branch 'origin/configuration-split'
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Configuration.ml | 15 |
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 |