From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 14 Oct 2009 13:35:24 +0000 (+0000)
Subject: ncheck is not erased
X-Git-Tag: make_still_working~3301
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=667640d70feb01f2a800b548fa019c92b103d75a;p=helm.git

ncheck is not erased
---

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index a67075a29..829806871 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -392,7 +392,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us
           (* XXX use the metasenv, if possible *)
       in
       guistuff.mathviewer#show_entry (`NCic (t,ctx,m,s));
-      [], "", parsed_text_length
+      [status, parsed_text], "", parsed_text_length
 
 let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac =
   let module MQ = MetadataQuery in