Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

Commit df417ca3 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

store loadpath as a set of paths, not as a list

Thanks to Johannes Kanig for the suggestion.
parent 2726d45a
......@@ -39,7 +39,7 @@ exception TheoryNotFound of pathname * string
exception AmbiguousPath of filename * filename
type env = {
env_path : filename list;
env_path : Sstr.t;
env_tag : Hashweak.tag;
}
......@@ -50,11 +50,11 @@ module Wenv = Hashweak.Make(struct type t = env let tag = env_tag end)
(** Environment construction and utilisation *)
let create_env = let c = ref (-1) in fun lp -> {
env_path = lp;
env_path = List.fold_right Sstr.add lp Sstr.empty;
env_tag = (incr c; Hashweak.create_tag !c)
}
let get_loadpath env = env.env_path
let get_loadpath env = Sstr.elements env.env_path
let read_format_table = Hashtbl.create 17 (* format name -> read_format *)
let extensions_table = Hashtbl.create 17 (* suffix -> format name *)
......@@ -115,7 +115,7 @@ let locate_lib_file env path exts =
let add_ext ext = file ^ "." ^ ext in
let fl = if exts = [] then [file] else List.map add_ext exts in
let add_dir dir = List.map (Filename.concat dir) fl in
let fl = List.concat (List.map add_dir env.env_path) in
let fl = List.concat (List.map add_dir (get_loadpath env)) in
match List.filter Sys.file_exists fl with
| [] -> raise (LibFileNotFound path)
| [file] -> file
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment