Skip to content

Commit 3c53d0e

Browse files
committed
docs: trivial fixes
Some trivial fixes in manual.md like: - Add missing `(gdb) ` before GDB comments so that markdown tools don't take them as new title lines. - 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 3c53d0e

1 file changed

Lines changed: 4 additions & 3 deletions

File tree

docs/manual.md

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1177,9 +1177,9 @@ To boot a Microkit image, use a GDB prompt via openOCD per [seL4 Docs](https://d
11771177

11781178
2. Set the `a0` and `a1` registers for OpenSBI
11791179

1180-
# tell OpenSBI where DTB is (there is none)
1180+
(gdb) # tell OpenSBI where DTB is (there is none)
11811181
(gdb) set $a0=0
1182-
# tell OpenSBI that the default hart is #0
1182+
(gdb) # tell OpenSBI that the default hart is #0
11831183
(gdb) set $a1=0
11841184

11851185
3. Load OpenSBI's FW_JUMP payload targeted at `0x90000000`, implicitly setting the program counter.
@@ -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)