1 files changed, 0 insertions, 3 deletions
diff --git a/kernel/byterun/make_jumptbl.sh b/kernel/byterun/make_jumptbl.sh
deleted file mode 100755
index eacd4daac8..0000000000
--- a/kernel/byterun/make_jumptbl.sh
+++ /dev/null
@@ -1,3 +0,0 @@
-#!/usr/bin/env bash
-
-sed -n -e '/^  /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' -e '/^}/q' ${1} > ${2}