X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhbugs%2Ftutors%2Fhbugs_tutors_common.ml;h=dca58766a24900f743903bf9b45ddba50e90ac5a;hb=78cf601fd8b8dbb386b0db315dcbfdbe8256c15f;hp=8ffd4b7042e053f50227003c33f10b41dd6357df;hpb=05fb48fba4c9a1189bfba8eaa4fbb429f9e20b6c;p=helm.git

diff --git a/helm/hbugs/tutors/hbugs_tutors_common.ml b/helm/hbugs/tutors/hbugs_tutors_common.ml
index 8ffd4b704..dca58766a 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
 ;;  
@@ -202,8 +202,8 @@ module BuildTutor (Dsc: HbugsTutorDescription) : HbugsTutor =
               Hbugs_deity.kill slave_thread;
               Hashtbl.remove slaves musing_id
             with
-            | Hbugs_deity.Can_t_kill (pid, reason) ->
-              prerr_endline (sprintf "Unable to kill slave %d: %s" pid reason)
+            | Hbugs_deity.Can_t_kill (_, reason) ->
+                prerr_endline (sprintf "Unable to kill slave: %s" reason)
             | Not_found ->
                 prerr_endline (sprintf
                   "Can't find slave corresponding to musing %s, can't kill it"