From 3072b88e9549743005cdfcb06ac9eb8ecba12fed Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 19 Mar 2020 10:15:13 +0100
Subject: [PATCH] [server] never kill outside of request handlers
---
src/plugins/server/main.ml | 4 +---
1 file changed, 1 insertion(+), 3 deletions(-)
diff --git a/src/plugins/server/main.ml b/src/plugins/server/main.ml
index 976f0d47d54..c3442a8c87b 100644
--- a/src/plugins/server/main.ml
+++ b/src/plugins/server/main.ml
@@ -402,9 +402,7 @@ let run server =
Senv.feedback "Server shutdown." ;
emitter := nop ;
set_active false ;
- with
- | Killed -> ()
- | exn ->
+ with exn ->
Senv.feedback "Server interruped (fatal error)." ;
emitter := nop ;
set_active false ;
--
GitLab