X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fmatitadep.ml;h=48011c0b5300cde4643667d7be8bca91e9352b5b;hb=da59a744767c799ad287489c55f2ff972f93d93c;hp=0052199ec3cdc3984888af9b41952c7c31592e42;hpb=5b306342bf9befa57abd870527d6bd92b0a5ba50;p=helm.git

diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml
index 0052199ec..48011c0b5 100644
--- a/helm/matita/matitadep.ml
+++ b/helm/matita/matitadep.ml
@@ -23,6 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 module GA = GrafiteAst 
 module U = UriManager
 
@@ -50,16 +52,19 @@ let main () =
      (function
        | DependenciesParser.UriDep uri -> 
           let uri = UriManager.string_of_uri uri in
-          Hashtbl.add uri_deps ma_file uri
+          if not (Http_getter_storage.is_legacy uri) then
+            Hashtbl.add uri_deps ma_file uri
        | DependenciesParser.BaseuriDep uri -> 
           let uri = Http_getter_misc.strip_trailing_slash uri in
           Hashtbl.add baseuri_of ma_file uri
        | DependenciesParser.IncludeDep path -> 
           try 
             let baseuri =
-             DependenciesParser.baseuri_of_script ~include_paths path in
-            let moo_file = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in
-            Hashtbl.add include_deps ma_file moo_file
+              DependenciesParser.baseuri_of_script ~include_paths path in
+            if not (Http_getter_storage.is_legacy baseuri) then
+              let moo_file =
+                LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in
+              Hashtbl.add include_deps ma_file moo_file
           with Sys_error _ -> 
             HLog.warn 
               ("Unable to find " ^ path ^ " that is included in " ^ ma_file)