#include <R4300.h>
#include <bcp.h>

void
osBbPowerOn(void)
{
    IO_WRITE(PI_GPIO_REG, PI_GPIO_POWER_BIT|(PI_GPIO_POWER_BIT << PI_GPIO_ENABLE_SHIFT));
}

void
osBbPowerOff(void)
{
    IO_WRITE(PI_GPIO_REG, 0|(PI_GPIO_POWER_BIT << PI_GPIO_ENABLE_SHIFT));
}