On Monday 20 December 2010 21:50:34, Tom Tromey wrote: > + ui_out_table_header (uiout, 4, ui_left, "id", "Id"); > + ui_out_table_header (uiout, 17, ui_left, "target-id", "Target ID"); IMO, you should make up your mind on "Id" vs "ID". -- Pedro Alves