X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fprobe%2FmatitaList.ml;h=95250b26c13a65888f4af69635227353b7afcd1c;hb=ea99a55173ebdcfe60f3b3d6f6c979f5d7785d48;hp=d6426e361244313b067c1994aa8f2fb70a26b049;hpb=2f19651bcec24abfb1bf15ff7e1387daad1f6638;p=helm.git diff --git a/matita/components/binaries/probe/matitaList.ml b/matita/components/binaries/probe/matitaList.ml index d6426e361..95250b26c 100644 --- a/matita/components/binaries/probe/matitaList.ml +++ b/matita/components/binaries/probe/matitaList.ml @@ -1,12 +1,12 @@ (* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) module A = Array @@ -21,6 +21,7 @@ module H = HExtlib module O = Options module E = Engine +module X = Error let chop_extension file = try F.chop_extension file @@ -88,8 +89,8 @@ let from_uri base devel uri = let file = mk_file path in if Y.file_exists (F.concat base file) then scan_entry (is_script devel) base devel file - else E.missing path - else E.unsupported protocol + else X.missing path + else X.unsupported protocol let from_string base devel s = from_uri base devel (U.uri_of_string s)