]> matita.cs.unibo.it Git - helm.git/commitdiff
Debugging code commented out.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 22 Nov 2010 21:52:04 +0000 (21:52 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 22 Nov 2010 21:52:04 +0000 (21:52 +0000)
helm/software/components/grafite_engine/grafiteEngine.ml

index 976b25b55a79f8e7c6f3659777481b1ccaa9a4de..703e99222d3cdd4e3cb111012b3fd603dae99043 100644 (file)
@@ -888,7 +888,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
           | _ -> obj_kind
         in
         let obj = uri,height,[],[],obj_kind in
-        prerr_endline ("pp new obj \n"^NCicPp.ppobj obj);
+        (*prerr_endline ("pp new obj \n"^NCicPp.ppobj obj);*)
         let old_status = status in
         let status = NCicLibrary.add_obj status obj in
         let index_obj =