#ifndef SYSCALL_SCHED_H_
#define SYSCALL_SCHED_H_

#include <stdint.h>
#include "syscall.h"

int32_t SYSCALL0(sys_schedrelease);

#endif // SYSCALL_SCHED_H_