]> matita.cs.unibo.it Git - helm.git/commitdiff
out of sync w.r.t. configuration.ml
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 22 Nov 2001 13:16:15 +0000 (13:16 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 22 Nov 2001 13:16:15 +0000 (13:16 +0000)
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;;