Add gitdist --dist-help=default-branch to developers guide (#235)

TriBITSPub · Nov 3, 2017 · bb5715b · bb5715b
1 parent 6c16fcb
commit bb5715b
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 0 deletions.
diff --git a/tribits/doc/developers_guide/TribitsDevelopersGuide.rst b/tribits/doc/developers_guide/TribitsDevelopersGuide.rst
@@ -8631,6 +8631,7 @@ from `gitdist --help`_ and ``gitdist --dist-help=<topic>``:
 * `gitdist --dist-help=dist-repo-status`_
 * `gitdist --dist-help=repo-versions`_
 * `gitdist --dist-help=aliases`_
+* `gitdist --dist-help=default-branch`_
 * `gitdist --dist-help=usage-tips`_
 * `gitdist --dist-help=script-dependencies`_
 * `gitdist --dist-help=all`_
@@ -8675,6 +8676,12 @@ gitdist --dist-help=aliases
 .. include:: gitdist-dist-help-aliases.txt
    :literal:
 
+gitdist --dist-help=default-branch
+++++++++++++++++++++++++++++++++++
+
+.. include:: gitdist-dist-help-default-branch.txt
+   :literal:
+
 gitdist --dist-help=usage-tips
 ++++++++++++++++++++++++++++++
 

diff --git a/tribits/doc/developers_guide/generate-dev-guide.sh b/tribits/doc/developers_guide/generate-dev-guide.sh
@@ -115,6 +115,7 @@ if [ "$TRIBITS_DEV_GUIDE_SKIP_OTHER_EXTRACTION" == "" ] ; then
   generate_gitdist_dist_help_topic dist-repo-status
   generate_gitdist_dist_help_topic repo-versions
   generate_gitdist_dist_help_topic aliases
+  generate_gitdist_dist_help_topic default-branch
   generate_gitdist_dist_help_topic usage-tips
   generate_gitdist_dist_help_topic script-dependencies
   generate_gitdist_dist_help_topic all