+ if (elf_flags & E_M68HC11_F64)
+ {
+ set_gdbarch_double_bit (gdbarch, 64);
+ set_gdbarch_double_format (gdbarch, floatformats_ieee_double);
+ }
+ else
+ {
+ set_gdbarch_double_bit (gdbarch, 32);
+ set_gdbarch_double_format (gdbarch, floatformats_ieee_single);
+ }