aboutsummaryrefslogtreecommitdiffstats
path: root/checklink
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2014-12-04 16:06:25 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2014-12-04 16:06:25 +0100
commit2d3330d132b22db7dd44399e0aac6e9e60470f59 (patch)
treeb382424725a7faf65bb6ca0016651d49a3c84ffe /checklink
parent00a5e1af73862b1b1aa29b5a07fe43f80f29c764 (diff)
downloadcompcert-2d3330d132b22db7dd44399e0aac6e9e60470f59.tar.gz
compcert-2d3330d132b22db7dd44399e0aac6e9e60470f59.zip
Removed more unused variables.
Diffstat (limited to 'checklink')
-rw-r--r--checklink/Check.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/checklink/Check.ml b/checklink/Check.ml
index c99a4db4..87910863 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -535,7 +535,6 @@ let check_label_existence ffw =
had the expected [size].
*)
let rec match_jmptbl lbllist vaddr size ffw =
- let atom = Hashtbl.find ffw.sf.atoms ffw.this_ident in
let rec match_jmptbl_aux lbllist bs ffw =
match lbllist with
| [] -> OK ffw