Fix doc build with texinfo 5.2