aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Configuration.ml
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2014-12-17 15:28:01 +0100
committerXavier Leroy <xavier.leroy@inria.fr>2014-12-17 15:28:01 +0100
commit4461db2bd92973b83bbd74c8f2eec16d702cffed (patch)
treeb02c8d646631662a5309238c13306a7d1f3e72db /driver/Configuration.ml
parent20c70573181f81c99ea4e8797615dac8308a9b18 (diff)
parentc1daedb244d1f7586c12749642b0d78ae910e60a (diff)
downloadcompcert-4461db2bd92973b83bbd74c8f2eec16d702cffed.tar.gz
compcert-4461db2bd92973b83bbd74c8f2eec16d702cffed.zip
Merge branch 'master' into pure-makefiles
Diffstat (limited to 'driver/Configuration.ml')
-rw-r--r--driver/Configuration.ml11
1 files changed, 8 insertions, 3 deletions
diff --git a/driver/Configuration.ml b/driver/Configuration.ml
index 1956b151..e73125f7 100644
--- a/driver/Configuration.ml
+++ b/driver/Configuration.ml
@@ -23,7 +23,7 @@ let _ =
open_in env_file
with Not_found ->
let dir = Sys.getcwd ()
- and name = Sys.argv.(0) in
+ and name = Sys.executable_name in
let dirname = if Filename.is_relative name then
Filename.dirname (Filename.concat dir name)
else
@@ -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