diff options
| -rw-r--r-- | cli/doc/.gitignore | 6 | ||||
| -rw-r--r-- | cli/doc/buildfile | 5 |
2 files changed, 7 insertions, 4 deletions
diff --git a/cli/doc/.gitignore b/cli/doc/.gitignore index 93bbd2d..84c93ab 100644 --- a/cli/doc/.gitignore +++ b/cli/doc/.gitignore @@ -1,5 +1,5 @@ +/cli.1 +/cli.xhtml + *.ps *.pdf - -/cli.xhtml -/cli.1 diff --git a/cli/doc/buildfile b/cli/doc/buildfile index af4ea97..8e40fe4 100644 --- a/cli/doc/buildfile +++ b/cli/doc/buildfile @@ -77,7 +77,7 @@ if $develop # Use the copyright year to approximate the last authoring date. # - ($<[0]) --generate-man $man_options \ + ($<[0]) --generate-man $man_options \ -v date="January $doc_year" \ --man-prologue-file $path($<[2]) \ --man-epilogue-file $path($<[3]) \ @@ -168,6 +168,9 @@ if $develop # to copy them since they are not stored in the repository, but let's do # that for consistency with the distributed source tree. # +# @@ TMP Note that cli-guide.xhtml and guide.html2ps still have copyright +# years hard-coded. +# ps{cli-guide}: xhtml{cli-guide} html2ps{guide} $html2ps { options = |