diff --git a/src/arch/i386/prefix/int19exit.c b/src/arch/i386/prefix/int19exit.c
index 282ece73..9696e133 100644
--- a/src/arch/i386/prefix/int19exit.c
+++ b/src/arch/i386/prefix/int19exit.c
@@ -1,13 +1,27 @@
 #include "bochs.h"
 #include "realmode.h"
 
-/**
+/** @file
+ *
  * The "exit via INT 19" exit path.
  *
  * INT 19 is the old (pre-BBS) "boot system" interrupt.  It is
  * conventionally used now to return from a failed boot from floppy
  * disk.
  *
+ */
+
+/**
+ * Exit via INT19
+ *
+ * @v ix86		i386 register values to be loaded on exit
+ * @ret Never
+ * @err None
+ *
+ * Exit back to the BIOS by switching to real mode, reloading the
+ * registers as they were before Etherboot started, and executing INT
+ * 19.
+ *
  * @bug Not yet implemented
  *
  */