diff options
Diffstat (limited to 'debugger/debugcom.ml')
| -rw-r--r-- | debugger/debugcom.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/debugger/debugcom.ml b/debugger/debugcom.ml index 72702da16..ac91df799 100644 --- a/debugger/debugcom.ml +++ b/debugger/debugcom.ml @@ -187,10 +187,10 @@ let set_trap_barrier pos = let value_size = if 1 lsl 31 = 0 then 4 else 8 let input_remote_value ic = - Misc.input_bytes ic value_size + really_input_string ic value_size let output_remote_value ic v = - output ic v 0 value_size + output_substring ic v 0 value_size exception Marshalling_error @@ -244,7 +244,7 @@ module Remote_value = if input_byte !conn.io_in = 0 then Remote(input_remote_value !conn.io_in) else begin - let buf = Misc.input_bytes !conn.io_in 8 in + let buf = really_input_string !conn.io_in 8 in let floatbuf = float n (* force allocation of a new float *) in String.unsafe_blit buf 0 (Obj.magic floatbuf) 0 8; Local(Obj.repr floatbuf) |