another insider trick

diff --git a/doc/doxygen/inside.doc b/doc/doxygen/inside.doc
index d39e3d2..03e3270 100644 (file)
--- a/doc/doxygen/inside.doc
+++ b/doc/doxygen/inside.doc
@@ -36,4 +36,7 @@ git will say so, and provide a ready to use patch that you can apply
 to improve your commit. Just carefully read the error message you get
 to find the exact command with git-apply to fix your formating.
 
+If you find that for a specific commit, the formatter does a very bad
+job, then add --no-verify to your git commit command line.
+
 */