On 09/05/2013 09:47 PM, Pedro Alves wrote: > I fixed them, and pushed the series in. Gah, and completely forgot to 'cvs add' all the new headers, so the gdbserver build is broken now for everyone. :-/ Now fixed... /me longs for 'git push'. -- Pedro Alves