diff options
| author | Boris Kolpackov <boris@codesynthesis.com> | 2022-09-08 14:59:33 +0200 |
|---|---|---|
| committer | Boris Kolpackov <boris@codesynthesis.com> | 2022-09-08 14:59:33 +0200 |
| commit | 7f739f0bf20ec6ce47174c244c3571cdea247c86 (patch) | |
| tree | ca6ff93044ff19811b4b6630703d4698742fe057 /cli | |
| parent | 9898d667145c800dab0d185d5c29d4bd2c0408a1 (diff) | |
Add note to cli/doc/buildfile
Diffstat (limited to 'cli')
| -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 { |