When I make web with today's git, all the urls in the generated web pages are missing the .html extensions (I did a full make clean and autogen.sh and the problem was still there). For example, from [1], the "User manual" link goes to [2] instead of [3].