aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Configuration.ml
diff options
context:
space:
mode:
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