diff options
Diffstat (limited to 'cli/doc/buildfile')
| -rw-r--r-- | cli/doc/buildfile | 6 |
1 files changed, 4 insertions, 2 deletions
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 { |