]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/hbugs/tutors/search_pattern_apply_tutor.ml
- implemented real thread killing (in place of the previous fake implementation)
[helm.git] / helm / hbugs / tutors / search_pattern_apply_tutor.ml
index 26183e2b97711e4a05c68facdc585e13256b5b88..be2c68d702c00b7d337a68f2e6bfe7e3446226c6 100644 (file)
@@ -72,9 +72,8 @@ let hbugs_callback mqi_handle =
         prerr_endline "received Start_musing";
         let new_musing_id = Hbugs_id_generator.new_musing_id () in
         let id = Hbugs_deity.create (slave mqi_handle) (state, new_musing_id) in
-        prerr_endline
-         (sprintf "starting a new musing (tid = %d, id = %s)" id new_musing_id);
-        Hashtbl.add ids new_musing_id id ;
+        prerr_endline (sprintf "starting a new musing (id = %s)" new_musing_id);
+        Hashtbl.add ids new_musing_id id;
         (*ignore (Thread.create slave (state, new_musing_id));*)
         Musing_started (my_own_id, new_musing_id)
       end else  (* broker unauthorized *)