From 6e3538235f0b82c074874ddfaa4526e06901256d Mon Sep 17 00:00:00 2001
From: "v.dijk.bas@gmail.com" <unknown>
Date: Thu, 20 Sep 2007 12:13:06 +0000
Subject: [PATCH] Removed duplicate entry for derbugging flag -ddump-tc from
 the user guide

---
 docs/users_guide/debugging.xml |   10 ----------
 1 file changed, 10 deletions(-)

diff --git a/docs/users_guide/debugging.xml b/docs/users_guide/debugging.xml
index 8a4129b..4ab4379 100644
--- a/docs/users_guide/debugging.xml
+++ b/docs/users_guide/debugging.xml
@@ -60,16 +60,6 @@
 
 	    <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>
-- 
1.7.10.4