Not elegant, but blink the on-board LED 5 times at start-up using the little core on FreeRTOS:
// GPIOC24 is the blue LED.
// The datasheet page 536 says:
// Configure register GPIO_SWPORTA_DDR and set GPIO as input or output.
// When the output pin is configured, write the output value to the
// GPIO_SWPORTA_DR register to control the GPIO output level.
#define GPIO2 0x03022000
#define GPIO_SWPORTA_DR 0x000
#define GPIO_SWPORTA_DDR 0x004
*(uint32_t*)(GPIO2|GPIO_SWPORTA_DDR) = 1 << 24;
for (i = 0; i < 5; i++)
{
*(uint32_t*)(GPIO2|GPIO_SWPORTA_DR) = 1 << 24;
mdelay(100);
*(uint32_t*)(GPIO2|GPIO_SWPORTA_DR) = 0;
mdelay(100);
}