From ad8b8cb05c14b56785519db91ecbb0b6525a7c98 Mon Sep 17 00:00:00 2001 From: guan jian <148229859+rez5427@users.noreply.github.com> Date: Mon, 9 Sep 2024 17:26:52 +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