Skip to content

Commit 7422ca4

Browse files
committed
fix: Avoid double-printing of internal grader errors
1 parent a97f813 commit 7422ca4

File tree

1 file changed

+13
-0
lines changed

1 file changed

+13
-0
lines changed

src/grader/grader_cli.ml

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -60,6 +60,19 @@ let grade ?(print_result=false) ?dirname
6060
>>= fun (result, stdout_contents, stderr_contents, outcomes) ->
6161
flush stderr;
6262
match result with
63+
| Error (Grading.Internal_error _ as err) ->
64+
let dump_error ppf =
65+
Format.fprintf ppf "%s@." (Grading.string_of_err err)
66+
in
67+
begin match dump_outputs with
68+
| None -> ()
69+
| Some prefix ->
70+
let oc = open_out (prefix ^ ".error") in
71+
dump_error (Format.formatter_of_out_channel oc) ;
72+
close_out oc
73+
end ;
74+
dump_error Format.err_formatter ;
75+
Lwt.return (Error (-1))
6376
| Error err ->
6477
let dump_error ppf =
6578
Format.fprintf ppf "%s@." (Grading.string_of_err err);

0 commit comments

Comments
 (0)