From 3db2f94ee7303024ba962a2cc364dc86d73b806a Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Fri, 13 Sep 2013 15:44:18 +0000
Subject: STM pretty printer should never fail

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16777 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/stm.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index b71b5c4be0..e050a5f363 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -372,11 +372,13 @@ end = struct (* {{{ *)
       | Some x -> job := None; Mutex.unlock m; x
 
     let run_command () =
-      while true do get_last_job () () done
+      try while true do get_last_job () () done
+      with e -> () (* No failure *)
 
     let command job =
       set_last_job job;
-      if Option.is_empty !worker then worker := Some (Thread.create run_command ())
+      if Option.is_empty !worker then
+        worker := Some (Thread.create run_command ())
 
   end (* }}} *)
 
@@ -675,7 +677,8 @@ end = struct (* {{{ *)
   let queue : task TQueue.t = TQueue.create ()
 
   let wait_all_done () =
-    TQueue.wait_until_n_are_waiting_and_queue_empty (SlavesPool.n_slaves ()) queue
+    TQueue.wait_until_n_are_waiting_and_queue_empty
+      (SlavesPool.n_slaves ()) queue
 
   let build_proof ~exn_info ~start ~stop =
     if SlavesPool.is_empty () then
-- 
cgit v1.2.3