X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatitac.ml;h=199b041576550d2a1b952dd96e5ef2112087238d;hb=4a62bde42e3655a7829b9281d9b9057dc32c0471;hp=968bdf505700a2c63934259493cbaa878b2bf960;hpb=c780c9756b67d116b1d5b5149ae758fa613c5fe6;p=helm.git

diff --git a/matita/matitac.ml b/matita/matitac.ml
index 968bdf505..199b04157 100644
--- a/matita/matitac.ml
+++ b/matita/matitac.ml
@@ -101,11 +101,9 @@ let main_compiler () =
          HLog.error ("Too many roots found, move into one and retry: "^
            String.concat ", " roots);exit 1);
     | [hd] -> 
-      let root, buri, file = Librarian.baseuri_of_script hd in
-      Make.load_deps_file (root ^ "/depends"),
-      let target = HExtlib.chop_prefix (root^"/") file in
+      let root, buri, file, target = Librarian.baseuri_of_script hd in
       HLog.debug ("Compiling target '" ^ target ^ "' with base uri '"^buri^"'");
-      [target]
+      Make.load_deps_file (root ^ "/depends"), [target]
     | _ -> HLog.error "Only one target (or none) can be specified.";exit 1
   in
   (* must be called after init since args are set by cmdline parsing *)