summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorKaren Arutyunov <karen@codesynthesis.com>2020-07-29 16:01:39 +0300
committerKaren Arutyunov <karen@codesynthesis.com>2020-12-06 20:32:32 +0300
commit95d9bd5dfa84625662c5f5a06d902f136a6e15aa (patch)
tree9996e5fab6faff7bfe6081f8a0a3c1ac5f92a8c9
parente3dd3066562ec146ce406611375ed6337c13f7d1 (diff)
Fix doc/buildfileci
-rw-r--r--cli/doc/buildfile4
1 files changed, 2 insertions, 2 deletions
diff --git a/cli/doc/buildfile b/cli/doc/buildfile
index 78f0e62..10e3536 100644
--- a/cli/doc/buildfile
+++ b/cli/doc/buildfile
@@ -53,7 +53,7 @@ if ($cli != [null])
clean = ($src_root != $out_root)
}
{{
- diag cli $>: ($<[0])
+ diag cli $> : ($<[0]) # @@ TMP
# Note that the date change doesn't change the script semantics, thus the
# variable is defined locally.
@@ -74,7 +74,7 @@ if ($cli != [null])
clean = ($src_root != $out_root)
}
{{
- diag cli $>: ($<[0])
+ diag cli $> : ($<[0]) # @@ TMP
$cli --generate-html $man_options \
--html-prologue-file $path($<[1]) \
--html-epilogue-file $path($<[2]) \