From 7f739f0bf20ec6ce47174c244c3571cdea247c86 Mon Sep 17 00:00:00 2001 From: Boris Kolpackov Date: Thu, 8 Sep 2022 14:59:33 +0200 Subject: Add note to cli/doc/buildfile --- cli/doc/buildfile | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'cli') diff --git a/cli/doc/buildfile b/cli/doc/buildfile index 61dfd4f..af4ea97 100644 --- a/cli/doc/buildfile +++ b/cli/doc/buildfile @@ -163,8 +163,10 @@ if $develop # {ps pdf}{cli-guide}: dist = ($html2pdf ? pregenerated/ : false) -# Note: the pregenerated file may not exist, thus --no-cleanup option is -# required for the cp builtin call. +# Note: the pregenerated files may not exist, thus --no-cleanup option is +# required for the cp builtin call. Strictly speaking we don't really need +# to copy them since they are not stored in the repository, but let's do +# that for consistency with the distributed source tree. # ps{cli-guide}: xhtml{cli-guide} html2ps{guide} $html2ps { -- cgit v1.1