Index: kernel/arch/ia32/src/vreg.c
===================================================================
--- kernel/arch/ia32/src/vreg.c	(revision af9dd1ed6f5d79cc098da33ff7131162b1c177a4)
+++ kernel/arch/ia32/src/vreg.c	(revision b0e014061cbe1c8f1aa804f8e1a40344f95c6af1)
@@ -51,4 +51,8 @@
 uint32_t *vreg_ptr = &vreg_tp_dummy;
 
+/**
+ * Allocate and initialize a per-CPU user page to be accessible via the GS
+ * segment register and to hold the virtual registers.
+ */
 void vreg_init(void)
 {