aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqtop.ml')
-rw-r--r--toplevel/coqtop.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 076db5e11..d41ecebe0 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -359,7 +359,8 @@ let get_int opt n =
let get_host_port opt s =
match CString.split ':' s with
- | [host; port] -> Some (Spawned.Socket(host, int_of_string port))
+ | [host; portr; portw] ->
+ Some (Spawned.Socket(host, int_of_string portr, int_of_string portw))
| ["stdfds"] -> Some Spawned.AnonPipe
| _ ->
prerr_endline ("Error: host:port or stdfds expected after option "^opt);