From 44080f418c87583c71c816f4c34a2bffea90bab5 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 19 Feb 2010 07:38:54 +0000 Subject: [PATCH] added lazy --- helm/software/components/ng_tactics/nnAuto.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml index ec92ff135..d719b8a96 100644 --- a/helm/software/components/ng_tactics/nnAuto.ml +++ b/helm/software/components/ng_tactics/nnAuto.ml @@ -1477,7 +1477,7 @@ let height_of_goals status = ) context) open_goals; - debug_print ("altezza sequente: " ^ string_of_int !h); + debug_print (lazy ("altezza sequente: " ^ string_of_int !h)); !h ;; -- 2.39.2