Concrete spaces do form a category, after all :-)

[helm.git] / helm / software / matita / matitacLib.ml

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index 99c132c11d27cf2a6f951ef71087bc26aadaf172..9c331d2ee2da2bf2a0bc9d692aa9c58543c4f451 100644 (file)
--- 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