equal
deleted
inserted
replaced
52 val input_file = filename dir "sos_in" |
52 val input_file = filename dir "sos_in" |
53 val _ = File.write input_file input |
53 val _ = File.write input_file input |
54 |
54 |
55 (* call solver *) |
55 (* call solver *) |
56 val output_file = filename dir "sos_out" |
56 val output_file = filename dir "sos_out" |
57 val (output, rv) = system_out ( |
57 val (output, rv) = |
58 if File.exists cmd then space_implode " " |
58 bash_output |
59 [File.shell_path cmd, File.shell_path input_file, File.shell_path output_file] |
59 (if File.exists cmd then |
60 else error ("Bad executable: " ^ File.platform_path cmd)) |
60 space_implode " " |
|
61 [File.shell_path cmd, File.shell_path input_file, File.shell_path output_file] |
|
62 else error ("Bad executable: " ^ File.platform_path cmd)) |
61 |
63 |
62 (* read and analyze output *) |
64 (* read and analyze output *) |
63 val (res, res_msg) = find_failure rv |
65 val (res, res_msg) = find_failure rv |
64 val result = if File.exists output_file then File.read output_file else "" |
66 val result = if File.exists output_file then File.read output_file else "" |
65 |
67 |