The HISTORY, LICENSE and CONTRIBUTORS files are not longer generated.

diff --git a/doc/Makefile.in b/doc/Makefile.in
index e73a4fd091d32b3979236f3a5f90b88d592448ca..e2c1ef8a40b961c4ae24734fda6e92918ffe374f 100644 (file)
--- a/doc/Makefile.in
+++ b/doc/Makefile.in
@@ -74,8 +74,7 @@ DEVDOCS = $(srcdir)/sudo.man.in $(srcdir)/sudo.cat \
          $(srcdir)/sudoers.ldap.man.in $(srcdir)/sudoers.ldap.cat \
          $(srcdir)/sudoers.man.in $(srcdir)/sudoers.cat \
          $(srcdir)/sudoreplay.man.in $(srcdir)/sudoreplay.cat \
-         $(srcdir)/sudo_plugin.man.in $(srcdir)/sudo_plugin.cat \
-         $(srcdir)/HISTORY $(srcdir)/LICENSE $(srcdir)/CONTRIBUTORS
+         $(srcdir)/sudo_plugin.man.in $(srcdir)/sudo_plugin.cat
 
 OTHER_DOCS = $(top_srcdir)/ChangeLog $(top_srcdir)/README \
             $(top_srcdir)/NEWS $(srcdir)/HISTORY $(srcdir)/CONTRIBUTORS \