[PATCH] Add machine type to gdbarch_register_osbi

[Eli Zaretskii]

> Date: Sun, 22 Dec 2002 19:25:09 +0100 (CET)
> From: Mark Kettenis <kettenis@chello.nl>
> 
>    Is this function documented in gdbint.texinfo?  If so, the docs needs to 
>    be updated as well.
> 
> How about the attached patch?

Perfect, thanks.