*** texinfo.txi~	2013-01-01 20:31:56.000000000 +0100
--- texinfo.txi	2013-01-02 10:33:26.000000000 +0100
***************
*** 10262,10268 ****
  * syncodeindex::                How to merge two indices, using @code{@@code}
                                   font for the merged-from index.
  * synindex::                    How to merge two indices, using the
!                                  default font of the merged-to index.
  @end menu
  
  
--- 10262,10268 ----
  * syncodeindex::                How to merge two indices, using @code{@@code}
                                   font for the merged-from index.
  * synindex::                    How to merge two indices, using the
!                                  roman font for the merged-from index.
  @end menu