void do_nothing(int)
{
}