aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Configuration.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-08-23 19:43:14 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2015-08-23 19:43:14 +0200
commitc879cd9abb6e5dac1bc303da1b0c11e551d8528e (patch)
treea72504985b0a5f5e4ac2971b4f853b4085985826 /driver/Configuration.ml
parentc6567a3f0a16050fd04469fdcc7a575f81c0c8f4 (diff)
downloadcompcert-kvx-c879cd9abb6e5dac1bc303da1b0c11e551d8528e.tar.gz
compcert-kvx-c879cd9abb6e5dac1bc303da1b0c11e551d8528e.zip
Added the directory ../share/compcert to the search path for .ini files and replaced the if else for the different possibilities by a List.find.
Diffstat (limited to 'driver/Configuration.ml')
-rw-r--r--driver/Configuration.ml21
1 files changed, 12 insertions, 9 deletions
diff --git a/driver/Configuration.ml b/driver/Configuration.ml
index 64f24820..41325368 100644
--- a/driver/Configuration.ml
+++ b/driver/Configuration.ml
@@ -20,17 +20,20 @@ let ini_file_name =
Sys.getenv "COMPCERT_CONFIG"
with Not_found ->
let exe_dir = Filename.dirname Sys.executable_name in
- let exe_ini = Filename.concat exe_dir "compcert.ini" in
let share_dir =
Filename.concat (Filename.concat exe_dir Filename.parent_dir_name)
- "share" in
- let share_ini = Filename.concat share_dir "compcert.ini" in
- if Sys.file_exists exe_ini then exe_ini
- else if Sys.file_exists share_ini then share_ini
- else begin
- eprintf "Cannot find compcert.ini configuration file.\n";
- exit 2
- end
+ "share" in
+ let share_compcert_dir =
+ Filename.concat share_dir "compcert" in
+ let search_path = [exe_dir;share_dir;share_compcert_dir] in
+ let files = List.map (fun s -> Filename.concat s "compcert.ini") search_path in
+ try
+ List.find Sys.file_exists files
+ with Not_found ->
+ begin
+ eprintf "Cannot find compcert.ini configuration file.\n";
+ exit 2
+ end
(* Read in the .ini file *)