diff --git a/src/system/kernel/arch/x86/arch_user_debugger.cpp b/src/system/kernel/arch/x86/arch_user_debugger.cpp
index 92298f158d..f8dc9fa7b0 100644
--- a/src/system/kernel/arch/x86/arch_user_debugger.cpp
+++ b/src/system/kernel/arch/x86/arch_user_debugger.cpp
@@ -767,7 +767,7 @@ arch_clear_kernel_watchpoint(void *address)
 
 
 /**
- *	Interrupts are disabled.
+ *	Interrupts are disabled. \a frame is unused, i.e. can be \c NULL.
  */
 void
 x86_init_user_debug_at_kernel_exit(struct iframe *frame)