Put the default value for -dppr-user-length in the manual

	MERGE TO STABLE

Incidentally, this flag should probably be renamed -dppr-user-depth

diff --git a/docs/users_guide/debugging.xml b/docs/users_guide/debugging.xml
index 2a88767..8a4129b 100644 (file)
--- a/docs/users_guide/debugging.xml
+++ b/docs/users_guide/debugging.xml
@@ -429,7 +429,7 @@
          <para>In error messages, expressions are printed to a
          certain &ldquo;depth&rdquo;, with subexpressions beyond the
          depth replaced by ellipses.  This flag sets the
-         depth.</para>
+         depth.  Its default value is 5.</para>
        </listitem>
       </varlistentry>