summaryrefslogtreecommitdiff
path: root/doc/release.cli
diff options
context:
space:
mode:
authorBoris Kolpackov <boris@codesynthesis.com>2021-02-22 15:41:06 +0200
committerBoris Kolpackov <boris@codesynthesis.com>2021-02-22 15:41:06 +0200
commit261358a3c093002af8d7ed2405ee64b0bcd8b555 (patch)
tree88e4e7c5a053dc6336765ca081d9e904e012ce5a /doc/release.cli
parent55ff42d0144cb303d8a1b5c02e630c72e19ec517 (diff)
Fix formatting in bash guide
Diffstat (limited to 'doc/release.cli')
-rw-r--r--doc/release.cli4
1 files changed, 4 insertions, 0 deletions
diff --git a/doc/release.cli b/doc/release.cli
index 9a83a44..92d799e 100644
--- a/doc/release.cli
+++ b/doc/release.cli
@@ -52,6 +52,10 @@ distribution from \c{etc/stage} and add the pre-distributed packages
copyright update notification via a pre-commit hook. So perhaps this step
can be removed.
+\h#install-times|Update install script times.|
+
+ See c{private/install/build2-times.txt} for instructions.
+
\h#etc|Update \c{etc/git/modules}|
Review for any new modules. Remove \c{etc/} and \c{private/} from