redirect stderr to stdout
authorhaftmann
Wed Jul 14 09:42:44 2010 +0200 (2010-07-14)
changeset 37814120c6e2d7474
parent 37813 7c33f5c5c59c
child 37815 053d23f08946
redirect stderr to stdout
src/Tools/Code/code_target.ML
     1.1 --- a/src/Tools/Code/code_target.ML	Tue Jul 13 21:07:12 2010 +0100
     1.2 +++ b/src/Tools/Code/code_target.ML	Wed Jul 14 09:42:44 2010 +0200
     1.3 @@ -364,7 +364,7 @@
     1.4          val _ = file destination (serialize thy target (SOME 80)
     1.5            (SOME module_name) [] naming program cs);
     1.6          val cmd = make_command env_param destination module_name;
     1.7 -      in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd) <> 0
     1.8 +      in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
     1.9          then error ("Code check failed for " ^ target ^ ": " ^ cmd)
    1.10          else ()
    1.11        end;