Skip to content

Commit fc38be2

Browse files
committed
docs: trivial fixes
Some trivial fixes in manual.md like: - Add missing break in 10.2 so that list is correctly rendered in PDF version. Signed-off-by: Yanfeng Liu <yfliu2008@qq.com>
1 parent b5cd889 commit fc38be2

1 file changed

Lines changed: 2 additions & 1 deletion

File tree

docs/manual.md

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1811,6 +1811,7 @@ At build-time, the Microkit tool embeds the capDL specification that describe
18111811
all kernel objects that needs to be created. Then for each kernel object, the spec
18121812
describe what state they need to be in and what capabilities exist to that object
18131813
(i.e. who has access to this kernel object). For example, the spec would specify the:
1814+
18141815
- starting Instruction Pointer (IP), Stack Pointer (SP) and IPC buffer pointer of a Thread Control Block (TCB),
18151816
- page table structure and mapping attributes of an address space (VSpace),
18161817
- interrupts (IRQ),
@@ -1862,7 +1863,7 @@ In order to do this however, the Microkit tool needs to emulate how the seL4 ker
18621863
to obtain the list of free untyped objects that the kernel would give to the initial task.
18631864

18641865
While this is non-trivial to do, it comes with the useful property that if the tool
1865-
produces a valid image, there should be no errors upon initialising the system
1866+
produces a valid image, there should be no errors upon initialising the system.
18661867
If there are any errors with configuring the system (e.g running out of memory),
18671868
they will be caught at build-time. This can only reasonably be done due to the
18681869
static-architecture of Microkit systems.

0 commit comments

Comments
 (0)