src/Tools/Code/code_target.ML

         val destination = make_destination p;
         val _ = export (SOME destination) (invoke_serializer ctxt target_name (SOME 80)
           generatedN args program all_public syms);
         val cmd = make_command generatedN;
       in
-        if Isabelle_System.bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
+        if Isabelle_System.bash ("cd " ^ File.bash_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
         then error ("Code check failed for " ^ target_name ^ ": " ^ cmd)
         else ()
       end;
   in
     if getenv env_var = ""