extern void write_object(
    char *out_file_name);