1 /*
2  * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3  *
4  * SPDX-License-Identifier: BSD-2-Clause
5  */
6 
7 #pragma once
8 
9 #include <sel4/types.h>
10 #include <sel4/bootinfo_types.h>
11 #include <sel4/macros.h>
12 
13 void seL4_InitBootInfo(seL4_BootInfo *bi)
14 SEL4_DEPRECATED("libsel4 management of bootinfo is deprecated, see the BootInfo Frame section of the manual");
15 seL4_BootInfo *seL4_GetBootInfo(void)
16 SEL4_DEPRECATED("libsel4 management of bootinfo is deprecated, see the BootInfo Frame section of the manual");
17 
18