diff options
| -rwxr-xr-x | configure | 9 |
1 files changed, 9 insertions, 0 deletions
@@ -687,6 +687,8 @@ make_examples make_uninstall_otherdoc make_install_otherdoc make_otherdoc +make_uninstall_shipped_htmldoc +make_install_shipped_htmldoc doc_dist_target_ok YACC DVIPRINT @@ -6031,6 +6033,13 @@ fi $as_echo "$as_me: WARNING: Invalid \`--with-doc' argument: $i" >&2;} done fi + if test $docadd_html = yes; then + make_install_shipped_htmldoc=install_shipped_htmldoc + make_uninstall_shipped_htmldoc=uninstall_shipped_htmldoc + else + make_install_shipped_htmldoc= + make_uninstall_shipped_htmldoc= + fi if test $docadd_other = yes; then make_otherdoc=otherdoc make_install_otherdoc=install_otherdoc |