equal
deleted
inserted
replaced
71 execute (check_valid ^ " -dump-result " ^ |
71 execute (check_valid ^ " -dump-result " ^ |
72 File.shell_path svc_output_file ^ |
72 File.shell_path svc_output_file ^ |
73 " " ^ File.shell_path svc_input_file ^ |
73 " " ^ File.shell_path svc_input_file ^ |
74 ">/dev/null 2>&1")) |
74 ">/dev/null 2>&1")) |
75 val svc_output = |
75 val svc_output = |
76 (case Library.try File.read svc_output_file of |
76 (case try File.read svc_output_file of |
77 SOME out => out |
77 SOME out => out |
78 | NONE => error "SVC returned no output"); |
78 | NONE => error "SVC returned no output"); |
79 in |
79 in |
80 if ! trace then tracing ("SVC Returns:\n" ^ svc_output) |
80 if ! trace then tracing ("SVC Returns:\n" ^ svc_output) |
81 else (File.rm svc_input_file; File.rm svc_output_file); |
81 else (File.rm svc_input_file; File.rm svc_output_file); |