+# In reality, we do not depend on the .txt files, but on the corresponding .deflist's.
+# However, the Makefile language cannot express that doc-extract generates both .txt
+# and .deflist, so we always use the .txt's in dependencies.
+$(patsubst %.html,%.txt,$(DOC_INDICES)): $(o)/%.txt: $(patsubst %.html,%.txt,$(DOCS)) $(s)/build/doc-defs
+ $(M)"DOC-DEFS $@"