diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-12-15 16:18:05 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-12-15 16:18:05 +0100 |
| commit | 2fa738f7c3ea91734752bc47b14d8a461e4fd5c2 (patch) | |
| tree | 9b95ca257d2732673b27858c5f0232c64f8252f5 /driver/Configuration.ml | |
| parent | 0342889a01aa16162232b0a87a4eb10bdb852ba4 (diff) | |
| download | compcert-kvx-2fa738f7c3ea91734752bc47b14d8a461e4fd5c2.tar.gz compcert-kvx-2fa738f7c3ea91734752bc47b14d8a461e4fd5c2.zip | |
Stdlib path is ignored when the configuration has_runtime_lib is set to false.
Diffstat (limited to 'driver/Configuration.ml')
| -rw-r--r-- | driver/Configuration.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/driver/Configuration.ml b/driver/Configuration.ml index aff638e7..e73125f7 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -58,8 +58,6 @@ let get_config key = let bad_config key v = Printf.eprintf "Invalid value `%s' for configuation option `%s'\n" v key; exit 2 -let stdlib_path = get_config "stdlib_path" - let prepro = get_config "prepro" let asm = get_config "asm" let linker = get_config "linker" @@ -81,6 +79,13 @@ let has_runtime_lib = | "false" -> false | v -> bad_config "has_runtime_lib" v + +let stdlib_path = + if has_runtime_lib then + get_config "stdlib_path" + else + "" + let asm_supports_cfi = match get_config "asm_supports_cfi" with | "true" -> true |