diff options
Diffstat (limited to 'debugger/unix_tools.ml')
| -rw-r--r-- | debugger/unix_tools.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/debugger/unix_tools.ml b/debugger/unix_tools.ml index 5a2f225433..8cefd37e0d 100644 --- a/debugger/unix_tools.ml +++ b/debugger/unix_tools.ml @@ -28,7 +28,7 @@ let convert_address address = ADDR_INET ((try inet_addr_of_string host with Failure _ -> try (gethostbyname host).h_addr_list.(0) with Not_found -> - prerr_endline ("Unknown host : " ^ host); + prerr_endline ("Unknown host: " ^ host); failwith "Can't convert address"), (try int_of_string port with Failure _ -> prerr_endline "The port number should be an integer"; @@ -41,14 +41,14 @@ let convert_address address = (*** Report a unix error. ***) let report_error = function | Unix_error (err, fun_name, arg) -> - prerr_string "Unix error : '"; + prerr_string "Unix error: '"; prerr_string fun_name; prerr_string "' failed"; if String.length arg > 0 then (prerr_string " on '"; prerr_string arg; prerr_string "'"); - prerr_string " : "; + prerr_string ": "; prerr_endline (error_message err) | _ -> fatal_error "report_error: not a Unix error" |