aboutsummaryrefslogtreecommitdiffstats
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
parent5735f427bb0e6698eb946b961baadfed0fac31e5 (diff)
parent00a5e1af73862b1b1aa29b5a07fe43f80f29c764 (diff)
downloadcompcert-kvx-52b22c39bfb257add757c5efe26d28052a77964e.tar.gz
compcert-kvx-52b22c39bfb257add757c5efe26d28052a77964e.zip
Merge branch 'master' into dwarf
-rw-r--r--checklink/Check.ml5
-rw-r--r--driver/Configuration.ml2
2 files changed, 1 insertions, 6 deletions
diff --git a/checklink/Check.ml b/checklink/Check.ml
index 0876f881..c99a4db4 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -536,11 +536,6 @@ let check_label_existence ffw =
*)
let rec match_jmptbl lbllist vaddr size ffw =
let atom = Hashtbl.find ffw.sf.atoms ffw.this_ident in
- let jmptbl_section =
- match atom.a_sections with
- | [_; _; j] -> j
- | _ -> Section_jumptable
- in
let rec match_jmptbl_aux lbllist bs ffw =
match lbllist with
| [] -> OK ffw
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