#ifndef _DEVICES_ACLINT_IPI
#define _DEVICES_ACLINT_IPI

#include "gen/aclint.h"
#include "platform.h"
#include <stdint.h>

static void send_ipi(uint32_t target_core)
{
    set_aclint_msip(aclint, target_core, 1);
}
#endif /* _DEVICES_ACLINT_IPI */