fixed a typo (inside a comment)

[helm.git] / helm / hbugs / tutors / hbugs_tutors_common.ml

diff --git a/helm/hbugs/tutors/hbugs_tutors_common.ml b/helm/hbugs/tutors/hbugs_tutors_common.ml
index 2f186c15dcb1682906b38eda47f32734e594d7e9..dca58766a24900f743903bf9b45ddba50e90ac5a 100644 (file)
--- a/helm/hbugs/tutors/hbugs_tutors_common.ml
+++ b/helm/hbugs/tutors/hbugs_tutors_common.ml
@@ -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"