Both the init_timer() and timer_setup() APIs have been removed. This script will not be needed any more. Signed-off-by: Kees Cook <keescook@chromium.org>