Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

Commit 7e5e7a4c authored by MARCHE Claude's avatar MARCHE Claude
Browse files

args_wrapper: avoid use of Str library

parent b06f27ae
...@@ -273,10 +273,10 @@ let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.en ...@@ -273,10 +273,10 @@ let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.en
match l with match l with
| s :: tail -> | s :: tail ->
(try (try
let path, name = match Str.split (Str.regexp "\.") s with let path, name = match Strings.split '.' s with
| [name] -> [],name | [name] -> [],name
| path::[name] -> | path::[name] ->
let path = Str.split (Str.regexp "/") path in let path = Strings.split '/' path in
path, name path, name
| _ -> failwith "Ill-formed theory name" | _ -> failwith "Ill-formed theory name"
in in
......
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