#ifndef SYSCALL_DEVCTL_H_
#define SYSCALL_DEVCTL_H_

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

int32_t SYSCALL5(sys_devctl, devh1, cmd1, buffer1, len1, extra1);

#endif // SYSCALL_DEVCTL_H_