1/*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 * Copyright 2015, 2016 Hesham Almatary <heshamelmatary@gmail.com>
4 *
5 * SPDX-License-Identifier: BSD-2-Clause
6 */
7
8#pragma once
9
10#include <autoconf.h>
11#include <sel4/simple_types.h>
12
13#define seL4_WordBits        32
14typedef seL4_Uint32 seL4_Word;
15