--- doc/Makefile.in.orig 2002-01-05 01:39:59.000000000 +0800 +++ doc/Makefile.in 2002-01-05 01:47:24.000000000 +0800 @@ -80,14 +80,10 @@ echo " install-info --info-dir=${DESTDIR}${infodir} ${DESTDIR}${infodir}/${PACKAGE}.info";\ install-info --info-dir=${DESTDIR}${infodir} ${DESTDIR}${infodir}/${PACKAGE}.info || :;\ else : ; fi - ${INSTALL_DATA} ${srcdir}/${PACKAGE}/${PACKAGE}*.html ${DESTDIR}${htmldir} - ${INSTALL_DATA} ${srcdir}/${PACKAGE}.dvi ${DESTDIR}${dvidir}/${PACKAGE}.dvi installdirs : force ${MKDIR} ${DESTDIR}${datadir} ${MKDIR} ${DESTDIR}${infodir} - ${MKDIR} ${DESTDIR}${htmldir} - ${MKDIR} ${DESTDIR}${dvidir} uninstall : force @if (install-info --version && \