aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2014-12-04 15:16:55 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2014-12-04 15:16:55 +0100
commit00a5e1af73862b1b1aa29b5a07fe43f80f29c764 (patch)
treed71b62892da569c61ed1ca74cc6ef581d9bff248
parent114b2b5634a97e60e2590d20eac072594d846206 (diff)
downloadcompcert-kvx-00a5e1af73862b1b1aa29b5a07fe43f80f29c764.tar.gz
compcert-kvx-00a5e1af73862b1b1aa29b5a07fe43f80f29c764.zip
Removed unused variable and changed the search for the installation directory. Use Sys.executable_name instead of Sys.argv.(0).
-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