Merge branch 'jc/ident' into next

diff --git a/Documentation/git-rev-list.txt b/Documentation/git-rev-list.txt
index f9146f1900d48f904f6150888c140fd5f5e1912f..1c6146c7643ef273888b76def0891b8a7ad51c98 100644 (file)
--- a/Documentation/git-rev-list.txt
+++ b/Documentation/git-rev-list.txt
@@ -14,6 +14,7 @@ SYNOPSIS
             [ \--min-age=timestamp ]
             [ \--sparse ]
             [ \--no-merges ]
+            [ \--remove-empty ]
             [ \--all ]
             [ [ \--merge-order [ \--show-breaks ] ] | [ \--topo-order ] ]
             [ \--parents ]
@@ -80,6 +81,9 @@ OPTIONS
        (still subject to count and age limitation), but apply
        merge simplification nevertheless.
 
+--remove-empty::
+       Stop when a given path disappears from the tree.
+
 --all::
        Pretend as if all the refs in `$GIT_DIR/refs/` are
        listed on the command line as <commit>.