Re: [Hugs] #33: Extra files installed if docbook2html is not available