src/Tools/Code/code_target.ML
changeset 69906 55534affe445
parent 69784 24bbc4e30e5b
child 69998 c61f6bc9cf5c
     1.1 --- a/src/Tools/Code/code_target.ML	Sun Mar 10 15:16:45 2019 +0000
     1.2 +++ b/src/Tools/Code/code_target.ML	Sun Mar 10 15:16:45 2019 +0000
     1.3 @@ -422,8 +422,9 @@
     1.4          val _ = export_result ctxt (SOME (SOME destination)) 80
     1.5            (invoke_serializer ctxt target_name generatedN args program all_public syms)
     1.6          val cmd = make_command generatedN;
     1.7 +        val context_cmd = "cd " ^ File.bash_path p ^ " && " ^ cmd ^ " 2>&1";
     1.8        in
     1.9 -        if Isabelle_System.bash ("cd " ^ File.bash_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
    1.10 +        if Isabelle_System.bash context_cmd <> 0
    1.11          then error ("Code check failed for " ^ target_name ^ ": " ^ cmd)
    1.12          else ()
    1.13        end;