X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitacLib.ml;h=9c331d2ee2da2bf2a0bc9d692aa9c58543c4f451;hb=9e03c0de729a0c42cfdd55a2cee085a59f7632a8;hp=99c132c11d27cf2a6f951ef71087bc26aadaf172;hpb=99cf752a677eeeaf0c3a6eb8283ef2d3956adc23;p=helm.git

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index 99c132c11..9c331d2ee 100644
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -373,7 +373,11 @@ module F =
           let generated = Filename.chop_suffix fname ".mma" ^ ".ma" in
 	  let atexit = dump generated in
 	  let res = compile options fname in
-	  atexit res
+	  let r = atexit res in
+	  if r then r else begin
+	     Sys.remove generated;
+	     Printf.printf "rm %s\n" generated; flush stdout; r
+	  end
        else
           compile options fname