Merge branch 'js/info-man-path'

* js/info-man-path: Documentation: clarify meaning of --html-path, --man-path, and --info-path git: add --info-path and --man-path options Conflicts: Makefile