Skip to content

Commit bc82c64

Browse files
yf13midnightveil
authored andcommitted
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 3be0795 commit bc82c64

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
@@ -1817,6 +1817,7 @@ At build-time, the Microkit tool embeds the capDL specification that describe
18171817
all kernel objects that needs to be created. Then for each kernel object, the spec
18181818
describe what state they need to be in and what capabilities exist to that object
18191819
(i.e. who has access to this kernel object). For example, the spec would specify the:
1820+
18201821
- starting Instruction Pointer (IP), Stack Pointer (SP) and IPC buffer pointer of a Thread Control Block (TCB),
18211822
- page table structure and mapping attributes of an address space (VSpace),
18221823
- interrupts (IRQ),
@@ -1868,7 +1869,7 @@ In order to do this however, the Microkit tool needs to emulate how the seL4 ker
18681869
to obtain the list of free untyped objects that the kernel would give to the initial task.
18691870

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

0 commit comments

Comments
 (0)