X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fmatitac.ml;h=d0f5603e58a347655379f812d378fa34fb9483ee;hb=89fc31fc5cc01e8860cf67a8e096c24125370d31;hp=67a1742f07dc4efbdd3daaa0f421e1c580a1742e;hpb=2e17165ef9e63367cc290ad555145b4c22a4582b;p=helm.git

diff --git a/matita/matita/matitac.ml b/matita/matita/matitac.ml
index 67a1742f0..d0f5603e5 100644
--- a/matita/matita/matitac.ml
+++ b/matita/matita/matitac.ml
@@ -44,7 +44,14 @@ let main_compiler () =
          prerr_endline ("Too many roots found:\n\t" ^ String.concat "\n\t" roots);
          prerr_endline ("\nEnter one of these directories and retry");
          exit 1);
-    | _ -> targets
+    | _ ->
+      let map targets file =
+          if HExtlib.is_dir file then
+             let files = HExtlib.find ~test:(fun path -> Filename.check_suffix path ".ma") file in
+             files @ targets
+          else file :: targets
+      in
+      List.fold_left map [] (List.rev targets)
   in
   (* must be called after init since args are set by cmdline parsing *)
   let system_mode =  Helm_registry.get_bool "matita.system" in
@@ -56,8 +63,9 @@ let main_compiler () =
      (try
        ignore (MatitaEngine.assert_ng ~include_paths:[] t); true
       with
-       MatitaEngine.FailureCompiling _ -> false) && b
-     ) true targets
+       MatitaEngine.FailureCompiling (_,exn) ->
+        HLog.error (snd (MatitaExcPp.to_string exn)); false) && b
+   ) true targets
   then 
     (HLog.message "Compilation successful"; 0)
   else