/* Copyright (C) 1998 DJ Delorie, see COPYING.DJ for details */
void __register_frame_info(void *begin __attribute__((unused)),
                           void *object __attribute__((unused)) );
void __register_frame_info(void *begin __attribute__((unused)),
                           void *object __attribute__((unused)) )
{
}