diff --git a/src/plugins/server/main.ml b/src/plugins/server/main.ml index cdfd4058c19fbc1d5421f88fce69cb311d268957..85dca6f876f514080937c7f0d39678903f184857 100644 --- a/src/plugins/server/main.ml +++ b/src/plugins/server/main.ml @@ -158,7 +158,7 @@ let execute yield exec : _ response = with | Killed -> `Killed exec.id | Error msg -> `Error(exec.id,msg) - | exn -> + | exn when Cmdline.catch_at_toplevel exn -> Senv.warning "[%s] Uncaught exception:@\n%s" exec.request (Cmdline.protect exn) ; `Error(exec.id,Printexc.to_string exn)