From 34d2f477be65e3fd26bfb6d43a3dd0807274549b Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 8 Nov 2007 12:33:11 +0000
Subject: [PATCH] please, commit files with debug=false otherwise the
 distributed matita prints a ton of dust

---
 helm/software/components/tactics/destructTactic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/helm/software/components/tactics/destructTactic.ml b/helm/software/components/tactics/destructTactic.ml
index 2ea9e047c..1344e978f 100644
--- a/helm/software/components/tactics/destructTactic.ml
+++ b/helm/software/components/tactics/destructTactic.ml
@@ -41,7 +41,7 @@ module ET = EqualityTactics
 module DTI = DoubleTypeInference
 module FNG = FreshNamesGenerator
 
-let debug = true
+let debug = false
 let debug_print = 
   if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ())
 
-- 
2.39.2