From cd4851f8be071b85d2189832801736d77085b51a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Thu, 12 Mar 2015 23:34:15 +0100
Subject: Fixing bug #4055.

When lauching ideslave without configuring the communication channels,
instead of raising an anomaly which is never caught by the main loop, we
rather exit the process with a relevant error message.
---
 stm/spawned.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'stm/spawned.ml')

diff --git a/stm/spawned.ml b/stm/spawned.ml
index 18159288d..a8372195d 100644
--- a/stm/spawned.ml
+++ b/stm/spawned.ml
@@ -81,6 +81,7 @@ let init_channels () =
 
 let get_channels () =
   match !channels with
-  | None -> Errors.anomaly(Pp.str "init_channels not called")
+  | None ->
+    Printf.eprintf "Fatal error: ideslave communication channels not set.\n";
+    exit 1
   | Some(ic, oc) -> ic, oc
-
-- 
cgit v1.2.3