<2012-08-19> Correction pour compiler avec makeinfo 4.13.
Authored by: vincentb1 2012-08-19
Parent: [r1538]
Child: [r1540]
