diff --git a/libsel4/include/sel4/bootinfo_types.h b/libsel4/include/sel4/bootinfo_types.h
index b47260809..27bc69868 100644
--- a/libsel4/include/sel4/bootinfo_types.h
+++ b/libsel4/include/sel4/bootinfo_types.h
@@ -61,9 +61,11 @@ typedef struct {
     seL4_SlotRegion   ioSpaceCaps;     /* IOSpace caps for ARM SMMU */
     seL4_Uint8        initThreadCNodeSizeBits; /* initial thread's root CNode size (2^n slots) */
     seL4_Domain       initThreadDomain; /* Initial thread's domain ID */
+    seL4_Word         archInfo;        /* tsc freq on x86, unused on arm */
     seL4_SlotRegion   untyped;         /* untyped-object caps (untyped caps) */
     seL4_UntypedDesc  untypedList[CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS]; /* information about each untyped */
-    seL4_Word         archInfo; /* tsc freq on x86, unused on arm */
+    /* the untypedList should be the last entry in this struct, in order
+     * to make this struct easier to represent in other languages */
 } seL4_BootInfo;