From 34d2f477be65e3fd26bfb6d43a3dd0807274549b Mon Sep 17 00:00:00 2001 From: Enrico Tassi 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