diff options
Diffstat (limited to 'driver/Configuration.ml')
| -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 |