From 50a89eba6659192f25c3d512a8b09830329b3997 Mon Sep 17 00:00:00 2001 From: Dirk Hohndel Date: Tue, 5 May 2020 18:25:57 -0700 Subject: [PATCH] documentation: fix makefile This one was my fault, not Willems (since I edited his commit). Signed-off-by: Dirk Hohndel --- Documentation/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Documentation/Makefile b/Documentation/Makefile index 1df632af6..390c9c6a1 100644 --- a/Documentation/Makefile +++ b/Documentation/Makefile @@ -7,7 +7,7 @@ # submitting patches to the user manual, only submit the changes to the .txt # file - the maintainer will recreate the .html.git file -DOCNAMES = user-manual user-manual_es user-manual_fr user-manual_ru user-manual_nl mobile-manual mobile-manual-v3 +DOCNAMES = user-manual user-manual_es user-manual_fr user-manual_ru user-manual_nl mobile-manual-v2 mobile-manual-v3 HTMLDOCS = $(patsubst %,$(OUT)%.html,$(DOCNAMES)) TEXTDOCS = $(patsubst %,$(OUT)%.text,$(DOCNAMES))