From ce95d985e921a11a8d40a10f006554085b5e4a55 Mon Sep 17 00:00:00 2001 From: Yui5427 <785369607@qq.com> Date: Mon, 9 Sep 2024 16:25:36 +0800 Subject: [PATCH] remove duplicated print_rvfi_exec --- Makefile | 1 - 1 file changed, 1 deletion(-) diff --git a/Makefile b/Makefile index 13e55a720..03ef4aa4a 100644 --- a/Makefile +++ b/Makefile @@ -301,7 +301,6 @@ rvfi_preserve_fns=-c_preserve rvfi_set_instr_packet \ -c_preserve rvfi_get_int_data \ -c_preserve rvfi_zero_exec_packet \ -c_preserve rvfi_halt_exec_packet \ - -c_preserve print_rvfi_exec \ -c_preserve print_instr_packet \ -c_preserve print_rvfi_exec