aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cbytegen.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/cbytegen.ml')
-rw-r--r--kernel/cbytegen.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index d6b3a9596..7a40a4029 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -220,7 +220,7 @@ let pos_rel i r sz =
(* non-terminating instruction (branch, raise, return, appterm) *)
(* in front of it. *)
-let rec discard_dead_code cont = cont
+let discard_dead_code cont = cont
(*function
[] -> []
| (Klabel _ | Krestart ) :: _ as cont -> cont