diff --git a/src/plugins/server/server_batch.ml b/src/plugins/server/server_batch.ml index 2df2d4d2567d1649b23219aa05712a9886951398..4fc37a40aa6850f9a8dfcbf01313317f67356436 100644 --- a/src/plugins/server/server_batch.ml +++ b/src/plugins/server/server_batch.ml @@ -102,7 +102,13 @@ let execute () = List.iter begin fun file -> Senv.feedback "Script %S" file ; - let response = execute_batch (Js.from_file file) in + let response = + try + execute_batch (Js.from_file file) + with Yojson.Json_error msg -> + Senv.error "[batch] error in JSON file:@\n%s@." msg; + `Null + in let output = Filename.remove_extension file ^ ".out.json" in let output = match BatchOutputDir.get () with | "" -> output