aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2014-12-04 16:19:22 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2014-12-04 16:19:22 +0100
commitb1345b1d0efec39850fb91dcc7e12d341b1a24fd (patch)
treedc7fac675e473287e96a8ce38b129738b92e993b
parent52b22c39bfb257add757c5efe26d28052a77964e (diff)
parent2d3330d132b22db7dd44399e0aac6e9e60470f59 (diff)
downloadcompcert-b1345b1d0efec39850fb91dcc7e12d341b1a24fd.tar.gz
compcert-b1345b1d0efec39850fb91dcc7e12d341b1a24fd.zip
Merge branch 'master' into dwarf
-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