Removed duplicate entry for derbugging flag -ddump-tc from the user guide

diff --git a/docs/users_guide/debugging.xml b/docs/users_guide/debugging.xml
index 8a4129b..4ab4379 100644 (file)
--- a/docs/users_guide/debugging.xml
+++ b/docs/users_guide/debugging.xml
@@ -60,16 +60,6 @@
 
            <varlistentry>
              <term>
 
            <varlistentry>
              <term>

-               <option>-ddump-tc</option>:
-                <indexterm><primary><option>-ddump-tc</option></primary></indexterm>
-             </term>
-             <listitem>
-               <para>typechecker output</para>
-             </listitem>
-           </varlistentry>
-
-           <varlistentry>
-             <term>

                <option>-ddump-splices</option>:
                 <indexterm><primary><option>-ddump-splices</option></primary></indexterm>
              </term>
                <option>-ddump-splices</option>:
                 <indexterm><primary><option>-ddump-splices</option></primary></indexterm>
              </term>