aboutsummaryrefslogtreecommitdiffstats
path: root/driver
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2014-12-04 15:39:28 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2014-12-04 15:39:28 +0100
commit52b22c39bfb257add757c5efe26d28052a77964e (patch)
tree41350880d1f2a068b8f434331be2d4705d18061a /driver
parent5735f427bb0e6698eb946b961baadfed0fac31e5 (diff)
parent00a5e1af73862b1b1aa29b5a07fe43f80f29c764 (diff)
downloadcompcert-52b22c39bfb257add757c5efe26d28052a77964e.tar.gz
compcert-52b22c39bfb257add757c5efe26d28052a77964e.zip
Merge branch 'master' into dwarf
Diffstat (limited to 'driver')
-rw-r--r--driver/Configuration.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/driver/Configuration.ml b/driver/Configuration.ml
index 1956b151..aff638e7 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