remote-hg: force remote push

diff --git a/Documentation/CodingGuidelines b/Documentation/CodingGuidelines
index b1bfff630fc0ec22d68757ebab84e76ee5abbc2c..7e4d5716a62bf59e8f072163ebac3064dad323ae 100644 (file)
--- a/Documentation/CodingGuidelines
+++ b/Documentation/CodingGuidelines
@@ -237,6 +237,9 @@ For Python scripts:
 
 Writing Documentation:
 
+ Most (if not all) of the documentation pages are written in AsciiDoc
+ and processed into HTML output and manpages.
+
  Every user-visible change should be reflected in the documentation.
  The same general rule as for code applies -- imitate the existing
  conventions.  A few commented examples follow to provide reference