From 5453f45f964804ebb83024a744eea3b91818c8cc Mon Sep 17 00:00:00 2001 From: Michael Zanetti Date: Wed, 12 Jul 2017 11:16:45 +0200 Subject: [PATCH] nodoc, not nodocs --- debian/rules | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/debian/rules b/debian/rules index 8424e45e..ec0a8012 100755 --- a/debian/rules +++ b/debian/rules @@ -12,7 +12,7 @@ endif $(info Building with DEB_BUILD_OPTIONS: [${DEB_BUILD_OPTIONS}]) MAKE_TARGETS=all -ifeq (,$(filter nodocs,$(DEB_BUILD_OPTIONS))) +ifeq (,$(filter nodoc,$(DEB_BUILD_OPTIONS))) MAKE_TARGETS += doc endif