diff --git a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h index e5db965ff..42c259026 100644 --- a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h +++ b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h @@ -314,7 +314,7 @@ seL4_DebugRun(void (*userfn) (void *), void* userarg) #endif #if CONFIG_ENABLE_BENCHMARKS -static inline void +static inline seL4_Error seL4_BenchmarkResetLog(void) { seL4_Word unused0 = 0;