Commit 88ce0c36 authored by Johannes Kanig's avatar Johannes Kanig

improve handling of runstdin command

parent 11317218
......@@ -359,6 +359,7 @@ let call_on_file ~command ~limit ~res_parser ~printer_mapping
Hashtbl.add saved_data id save;
let timelimit = get_time limit in
let memlimit = get_mem limit in
let use_stdin = if use_stdin then Some fin else None in
Prove_client.send_request ~use_stdin ~id ~timelimit ~memlimit ~cmd;
ServerCall id
......
......@@ -95,7 +95,7 @@ let set_max_running_provers x =
let send_request ~use_stdin ~id ~timelimit ~memlimit ~cmd =
force_connect ();
let buf = Buffer.create 128 in
let servercommand = if use_stdin then "runstdin;" else "run;" in
let servercommand = if use_stdin <> None then "runstdin;" else "run;" in
Buffer.add_string buf servercommand;
Buffer.add_string buf (string_of_int id);
Buffer.add_char buf ';';
......@@ -106,6 +106,12 @@ let send_request ~use_stdin ~id ~timelimit ~memlimit ~cmd =
Buffer.add_char buf ';';
Buffer.add_string buf x)
cmd;
begin match use_stdin with
| None -> ()
| Some s ->
Buffer.add_char buf ';';
Buffer.add_string buf s
end;
Buffer.add_char buf '\n';
let s = Buffer.contents buf in
send_request_string s
......
......@@ -6,7 +6,7 @@ val set_max_running_provers : int -> unit
val connect : unit -> unit
val send_request :
use_stdin:bool ->
use_stdin:string option ->
id:int ->
timelimit:int ->
memlimit:int ->
......
......@@ -257,7 +257,7 @@ pid_t create_process(char* cmd,
unix_argv = (char**)malloc(sizeof(char*) * (argc + 2));
unix_argv[0] = cmd;
unix_argv[argc + 1] = NULL;
for (i = 0; i < argc; i++) {
for (i = 0; i < count; i++) {
unix_argv[i + 1] = argv[i];
}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment