diff --git a/src/plugins/server/main.ml b/src/plugins/server/main.ml index 86545e30e34c7f53eb15788a9cb93d433807848d..640e7b7c64c7e0c22aca238605cf2c8898b3454f 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 (* -------------------------------------------------------------------------- *)