From 06c82a363221fb14261fac87215b21d00ec0b1a1 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Wed, 4 Sep 2019 17:15:27 +0200
Subject: [PATCH] [Server] catch Sys.Break at server main loop
---
src/plugins/server/main.ml | 18 ++++++++++++------
1 file changed, 12 insertions(+), 6 deletions(-)
diff --git a/src/plugins/server/main.ml b/src/plugins/server/main.ml
index 86545e30e34..640e7b7c64c 100644
--- a/src/plugins/server/main.ml
+++ b/src/plugins/server/main.ml
@@ -287,18 +287,24 @@ let run ~pretty ?(equal=(=)) ~fetch () =
shutdown = false ;
} in
try
+ (* TODO: remove the following line once the Why3 signal handler is not
+ used anymore. *)
+ Sys.catch_break true;
signal true ;
Senv.feedback "Server running." ;
- while not server.shutdown do
- let activity = process server in
- if not activity then Unix.sleepf idle_s ;
- done ;
+ begin try
+ while not server.shutdown do
+ let activity = process server in
+ if not activity then Unix.sleepf idle_s ;
+ done ;
+ with Sys.Break -> () (* Ctr+C, just leave the loop normally *)
+ end;
Senv.feedback "Server shutdown." ;
signal false ;
- with err ->
+ with exn ->
Senv.feedback "Server interruped (fatal error)." ;
signal false ;
- raise err
+ raise exn
end
(* -------------------------------------------------------------------------- *)
--
GitLab