Skip to content
Snippets Groups Projects
Commit 0233f5c4 authored by Matthew Fernandez's avatar Matthew Fernandez Committed by Adrian Danis
Browse files

manual: Fix missing init thread domain in boot info.

parent 4e2d71aa
No related branches found
No related tags found
No related merge requests found
......@@ -105,6 +105,7 @@ of slots in the initial thread's CNode, starting with CPTR \texttt{start} and wi
\texttt{uint8\_t} & \texttt{initThreadCNodeSizeBits} & CNode size ($2^n$ slots) \\
\texttt{seL4\_Word} & \texttt{numDeviceRegions} & number of device memory regions \\
\texttt{seL4\_DeviceRegion[]} & \texttt{deviceRegions} & device memory regions (see \autoref{tab:device_region_struct}) \\
\texttt{uint32\_t} & \texttt{initThreadDomain} & domain of the initial thread (see \autoref{sec:domains}) \\
\bottomrule
\end{tabularx}
\end{center}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment