diff options
author | David Pursehouse <dpursehouse@digital.ai> | 2020-06-06 15:04:24 +0900 |
---|---|---|
committer | David Pursehouse <dpursehouse@digital.ai> | 2020-06-06 15:04:54 +0900 |
commit | 2ba3b5a55d37315189104d4237c007bae01f908d (patch) | |
tree | 68ffb7c6979915a6a0077405ea32b858e188b8b2 | |
parent | 9b2d1da73fd1a1dbe40d8bba9428194201a2ecf9 (diff) |
Fix header of "Pitfalls" subsection of Private Changes documentation
Change-Id: I3dacba7ffd910122cf1dbd123276c6ef29fe5f14
-rw-r--r-- | Documentation/intro-user.txt | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/Documentation/intro-user.txt b/Documentation/intro-user.txt index e502cdd1a3..6b5b543dca 100644 --- a/Documentation/intro-user.txt +++ b/Documentation/intro-user.txt @@ -605,8 +605,7 @@ In that case, care should be taken to prevent the CI system from exposing secret details. [[private-changes-pitfalls]] -Pitfalls -=== +=== Pitfalls If private changes are used, be aware of the following pitfalls: |