# HG changeset patch
# User haftmann
# Date 1279093364 -7200
# Node ID 120c6e2d74741d8e7d8ce71197e2e080c696c9cd
# Parent  7c33f5c5c59c6724f7e230acd2326ca497543227
redirect stderr to stdout

diff -r 7c33f5c5c59c -r 120c6e2d7474 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Tue Jul 13 21:07:12 2010 +0100
+++ b/src/Tools/Code/code_target.ML	Wed Jul 14 09:42:44 2010 +0200
@@ -364,7 +364,7 @@
         val _ = file destination (serialize thy target (SOME 80)
           (SOME module_name) [] naming program cs);
         val cmd = make_command env_param destination module_name;
-      in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd) <> 0
+      in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
         then error ("Code check failed for " ^ target ^ ": " ^ cmd)
         else ()
       end;