doc lei: drop an unnecessary to-do comment

[public-inbox.git] / Documentation / include.mk

diff --git a/Documentation/include.mk b/Documentation/include.mk
index 41de0a7277e3c38ab28cb0c5ac55c86626bf43d7..79bf460d22cfbf3f14bc4768e5eeb06d895a1ef3 100644 (file)
--- a/Documentation/include.mk
+++ b/Documentation/include.mk
@@ -1,4 +1,4 @@
-# Copyright (C) 2013-2019 all contributors <meta@public-inbox.org>
+# Copyright (C) 2013-2021 all contributors <meta@public-inbox.org>
 # License: AGPL-3.0+ <https://www.gnu.org/licenses/agpl-3.0.txt>
 all::
 
@@ -6,6 +6,7 @@ RSYNC = rsync
 RSYNC_DEST = public-inbox.org:/srv/public-inbox/
 AWK = awk
 MAN = man
+LEXGROG = lexgrog
 
 # this is "xml" on FreeBSD and maybe some other distros:
 XMLSTARLET = xmlstarlet
@@ -56,6 +57,8 @@ check_man = $(AWK) '{gsub(/\b./,"")}length>80{print;err=1}END{exit(err)}'\
 
 check-man :: $(check_80)
 
+check-lexgrog :: $(check_lexgrog)
+
 all :: $(docs)
 
 txt2pre = $(PERL) -I lib ./Documentation/txt2pre >$@
@@ -89,9 +92,6 @@ check :: NEWS .NEWS.atom.check NEWS.html
 
 html: $(docs_html)
 
-Documentation/.x:
-       mkdir -p $@
-
 doc: $(docs)
 
 %.gz: %