Index: kernel/arch/ppc32/src/ppc32.c
===================================================================
--- kernel/arch/ppc32/src/ppc32.c	(revision c22e964a598c0c20654391f6a11e7333830cbf37)
+++ kernel/arch/ppc32/src/ppc32.c	(revision 9cd98796ce2b79a13dae8d49fe37ce6be500f3b8)
@@ -52,4 +52,5 @@
 bootinfo_t bootinfo;
 
+/** Performs ppc32-specific initialization before main_bsp() is called. */
 void arch_pre_main(void)
 {