/* Turns on or off the red and/or green LED.  */
void BOARD_ledSet(uint8_t leds)
/* Turns on or off the red and/or green LED.  */
void BOARD_ledSet(uint8_t leds)
{
   if( rgbledEnable && leds != 0 ) {
      BOARD_rgbledSetRawColor( 0, 0, 0 );
      BOARD_rgbledEnable( false, 0xFF );
   }
   uint8_t pins[2] = { BOARD_RGBLED_GREEN_PIN, BOARD_RGBLED_RED_PIN };
   for( int i = 0; i < 2; i++ ) {
      if( ( (leds >> i) & 1 ) == 1 ) {
         GPIO_PinOutSet( BOARD_RGBLED_RED_PORT, pins[i] );
      }
      else {
         GPIO_PinOutClear( BOARD_RGBLED_RED_PORT, pins[i] );
      }
   }
   return;
}