From bba4ac5f03b77ec80e15db081709a63999d952ab Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 9 Jan 2006 13:52:55 +0000 Subject: [PATCH] do not generate deps for legacy URIs --- helm/matita/matitadep.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml index fdcc89aa9..48011c0b5 100644 --- a/helm/matita/matitadep.ml +++ b/helm/matita/matitadep.ml @@ -52,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) -- 2.39.2