]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/metadata/create2/touch/configuration.ml.in
out of sync w.r.t. configuration.ml
[helm.git] / helm / metadata / create2 / touch / configuration.ml.in
index d20a3c0c0e0cf872dcb42de6cd4ccdbacad15803..c743be135682299954bbfbdd1500dc0c96338269 100644 (file)
@@ -112,6 +112,8 @@ let tmp_dir       = read_configuration_var     "tmp_dir"
 let helm_dir      = read_configuration_var     "helm_dir";;
 let getter_url    = read_configuration_var_env "getter_url" "HELM_GETTER_URL";;
 let processor_url = read_configuration_var_env "processor_url" "HELM_PROCESSOR_URL";;
+let annotations_dir = read_configuration_var_env "annotations_dir" "HELM_ANNOTATIONS_DIR"
+let annotations_url = read_configuration_var_env "annotations_url" "HELM_ANNOTATIONS_URL"
 
 let _ = Hashtbl.clear vars;;