From 3f81a72dbdc7f2ffb17cc1ecd4e6a39270891c77 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 11 Feb 2004 17:05:27 +0000 Subject: [PATCH] Ported to Helm_registry. --- helm/hbugs/tutors/hbugs_tutors_common.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/hbugs/tutors/hbugs_tutors_common.ml b/helm/hbugs/tutors/hbugs_tutors_common.ml index 8ffd4b704..2f186c15d 100644 --- a/helm/hbugs/tutors/hbugs_tutors_common.ml +++ b/helm/hbugs/tutors/hbugs_tutors_common.ml @@ -79,7 +79,7 @@ let typecheck_loaded_proof metasenv bo ty = type xml_kind = Body | Type;; let mk_dtdname ~ask_dtd_to_the_getter dtd = if ask_dtd_to_the_getter then - Configuration.getter_url ^ "getdtd?uri=" ^ dtd + Helm_registry.get "getter.url" ^ "getdtd?uri=" ^ dtd else "http://mowgli.cs.unibo.it/dtd/" ^ dtd ;; -- 2.39.2