#include <stdio.h>

void flush_stdout(void)
{
    fflush(stdout);
}