From: Enrico Tassi Date: Wed, 23 May 2007 14:07:24 +0000 (+0000) Subject: changed the way environment variable can interfere with the registry. X-Git-Tag: 0.4.95@7852~461 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=abc2259866ce9284a577ba74eb38f13da7a05f3d;p=helm.git changed the way environment variable can interfere with the registry. --- diff --git a/components/registry/helm_registry.ml b/components/registry/helm_registry.ml index 3753232b6..64277415f 100644 --- a/components/registry/helm_registry.ml +++ b/components/registry/helm_registry.ml @@ -133,7 +133,7 @@ let set' ?(replace=false) registry ~key ~value = let unset registry = Hashtbl.remove registry -let env_var_of_key = Str.global_replace dot_rex "__" +let env_var_of_key s = String.uppercase (Str.global_replace dot_rex "_" s) let singleton = function | [] ->