From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Sun, 7 Sep 2003 09:46:14 +0000 (+0000)
Subject: commented out thread killing (we have to wait for a decent Thread.exit
X-Git-Tag: v0_0_1~25
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=44de0d194b6f4d890605f023aaafd95e541381f0

commented out thread killing (we have to wait for a decent Thread.exit
implementation)
---

diff --git a/helm/hbugs/tutors/hbugs_deity.ml b/helm/hbugs/tutors/hbugs_deity.ml
index ba6caa478..b1fa0f30d 100644
--- a/helm/hbugs/tutors/hbugs_deity.ml
+++ b/helm/hbugs/tutors/hbugs_deity.ml
@@ -83,18 +83,25 @@ let wrap_thread body =
 
 let creation_mutex = Mutex.create () ;;
 
+(* REAL IMPLEMENTATION NOT YET WORKING --ZACK
 let create body arg =
   do_critical creation_mutex (lazy (
       ignore (Thread.create (wrap_thread body) arg);
       Event.sync (Event.receive chan)
   ))
 ;;
+
 let kill pid =
   add_to_dead_threads_walking pid;
   try
     Unix.kill pid kill_signal
   with e -> raise (Can_t_kill (pid, Printexc.to_string e))
 ;;
+*)
+
+(* FAKE IMPLEMENTATION *)
+let create x y = let _ = Thread.create x y in ~-1 ;;
+let kill _ = () ;;
 
   (* block kill signal in main process *)
 ignore (Unix.sigprocmask Unix.SIG_BLOCK [ kill_signal ]) ;;