1 /*
2  * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3  *
4  * SPDX-License-Identifier: GPL-2.0-only
5  */
6 
7 #include <kernel/thread.h>
8 #include <arch/kernel/thread.h>
9 
Arch_postModifyRegisters(tcb_t * tptr)10 void Arch_postModifyRegisters(tcb_t *tptr)
11 {
12     Mode_postModifyRegisters(tptr);
13 }
14