diff options
| author | dzwdz | 2021-09-18 09:37:53 +0200 |
|---|---|---|
| committer | dzwdz | 2021-09-18 09:37:53 +0200 |
| commit | 8e757fae5aaece57755a98544f193bc2672966b3 (patch) | |
| tree | 37ac93907323941a3bb3de2edb2fc08ca821360e /src/kernel/types.h | |
| parent | 7a44fc5381dabb65dfdb667dc442108d0465799a (diff) | |
merge `kernel/types.h` and `init/types.h`
Diffstat (limited to 'src/kernel/types.h')
| -rw-r--r-- | src/kernel/types.h | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/src/kernel/types.h b/src/kernel/types.h deleted file mode 100644 index 44a0d46..0000000 --- a/src/kernel/types.h +++ /dev/null @@ -1,12 +0,0 @@ -#pragma once -#include <stdint.h> - -#define TYPES_INCLUDED - -#ifdef __CHECKER__ -# define __user __attribute__((noderef, address_space(__user))) -#else -# define __user -#endif - -typedef void __user * userptr_t; |