aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--driver/Configuration.ml13
1 files changed, 11 insertions, 2 deletions
diff --git a/driver/Configuration.ml b/driver/Configuration.ml
index 50e251c4..b9153c36 100644
--- a/driver/Configuration.ml
+++ b/driver/Configuration.ml
@@ -21,12 +21,18 @@ let search_argv key =
done;
!res
+let absolute_path base file =
+ if Filename.is_relative file then
+ Filename.concat base file
+ else
+ file
+
(* Locate the .ini file, which is either in the same directory as
the executable or in the directory ../share *)
let ini_file_name =
match search_argv "--conf" with
- | Some s -> s
+ | Some s -> absolute_path (Sys.getcwd ()) s
| None ->
try
Sys.getenv "COMPCERT_CONFIG"
@@ -47,6 +53,8 @@ let ini_file_name =
exit 2
end
+let ini_dir = Filename.dirname ini_file_name
+
(* Read in the .ini file *)
let _ =
@@ -104,7 +112,8 @@ let has_standard_headers =
| v -> bad_config "has_standard_headers" [v]
let stdlib_path =
if has_runtime_lib then
- get_config_string "stdlib_path"
+ let path = get_config_string "stdlib_path" in
+ absolute_path ini_dir path
else
""
let asm_supports_cfi =