SubmittingPatches: mention doc-diff

diff --git a/Documentation/doc-diff b/Documentation/doc-diff
index f483fe427cea4c82ebe69fc67f3a8efd3d53ec9c..6e285e648cc15905bc2b3336b3a351dc076e2dca 100755 (executable)
--- a/Documentation/doc-diff
+++ b/Documentation/doc-diff
@@ -1,4 +1,12 @@
 #!/bin/sh
+#
+# Build two documentation trees and diff the resulting formatted output.
+# Compared to a source diff, this can reveal mistakes in the formatting.
+# For example:
+#
+#   ./doc-diff origin/master HEAD
+#
+# would show the differences introduced by a branch based on master.
 
 OPTIONS_SPEC="\
 doc-diff [options] <from> <to> [-- <diff-options>]