equal
deleted
inserted
replaced
401 let |
401 let |
402 val destination = make_destination p; |
402 val destination = make_destination p; |
403 val _ = export (SOME destination) (invoke_serializer thy target (SOME 80) |
403 val _ = export (SOME destination) (invoke_serializer thy target (SOME 80) |
404 module_name args naming program names_cs); |
404 module_name args naming program names_cs); |
405 val cmd = make_command module_name; |
405 val cmd = make_command module_name; |
406 in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0 |
406 in |
|
407 if Isabelle_System.bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0 |
407 then error ("Code check failed for " ^ target ^ ": " ^ cmd) |
408 then error ("Code check failed for " ^ target ^ ": " ^ cmd) |
408 else () |
409 else () |
409 end; |
410 end; |
410 in if getenv env_var = "" |
411 in |
|
412 if getenv env_var = "" |
411 then if strict |
413 then if strict |
412 then error (env_var ^ " not set; cannot check code for " ^ target) |
414 then error (env_var ^ " not set; cannot check code for " ^ target) |
413 else warning (env_var ^ " not set; skipped checking code for " ^ target) |
415 else warning (env_var ^ " not set; skipped checking code for " ^ target) |
414 else Isabelle_System.with_tmp_dir "Code_Test" ext_check |
416 else Isabelle_System.with_tmp_dir "Code_Test" ext_check |
415 end; |
417 end; |