From 14272a83280a5957651867afa96291426f2bdbab Mon Sep 17 00:00:00 2001 From: Alexandre Moine Date: Fri, 24 May 2019 13:12:23 +0200 Subject: [PATCH] print all buffers --- src/grader/grading.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/grader/grading.ml b/src/grader/grading.ml index 96a45fb9a..2e060c689 100644 --- a/src/grader/grading.ml +++ b/src/grader/grading.ml @@ -84,10 +84,9 @@ let get_grade !flush_stderr () ; !flush_stdout () ; let msg = - Buffer.contents stderr_buffer ^ - "\n" ^ - Buffer.contents stdout_buffer in - fail { Toploop_ext.msg ; locs = [] ; if_highlight = msg } + String.concat "\n" + (List.map Buffer.contents [stderr_buffer; stdout_buffer; outcomes_buffer]) + in fail { Toploop_ext.msg ; locs = [] ; if_highlight = msg } end | Toploop_ext.Error (err, w) -> warn w ;