texinfo7: 7.1.1 -> 7.2 (#368000)
authored by Wolfgang Walther and committed by GitHub 11 months ago eb4231f3 1bb42223