]> matita.cs.unibo.it Git - helm.git/commitdiff
commented out thread killing (we have to wait for a decent Thread.exit
authorStefano Zacchiroli <zack@upsilon.cc>
Sun, 7 Sep 2003 09:46:14 +0000 (09:46 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Sun, 7 Sep 2003 09:46:14 +0000 (09:46 +0000)
implementation)

helm/hbugs/tutors/hbugs_deity.ml

index ba6caa478c12b8d6a36c04f5abac9ae1f7170b70..b1fa0f30db910f4d9759b124a14fcc1efd7ca7fc 100644 (file)
@@ -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 ]) ;;