Function debug_int_write

src/engine/debugger.cpp:135–139

}

static void debug_int_write( FILE * out, int i )
{
    fprintf( out, "%d", i );
    fputc( '\0', out );
}

static int debug_int_read( FILE * in )
{