diff options
author | Pierre Weis <Pierre.Weis@inria.fr> | 2000-03-06 22:12:09 +0000 |
---|---|---|
committer | Pierre Weis <Pierre.Weis@inria.fr> | 2000-03-06 22:12:09 +0000 |
commit | b96208b7a247cbb6d9d162fbfaf54448af33589c (patch) | |
tree | a63fb52f6e36ca47129637586cf6d0fd3d576733 /debugger/unix_tools.ml | |
parent | a56ae9a35f7cb4b5ccd128c2b9610b4913d71331 (diff) |
Revu les impressions du compilateur
git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@2908 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
Diffstat (limited to 'debugger/unix_tools.ml')
-rw-r--r-- | debugger/unix_tools.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/debugger/unix_tools.ml b/debugger/unix_tools.ml index ec4f4079c..9de33ca5b 100644 --- a/debugger/unix_tools.ml +++ b/debugger/unix_tools.ml @@ -40,7 +40,7 @@ let convert_address address = (*** Report an unix error. ***) let report_error = function - Unix_error (err, fun_name, arg) -> + | Unix_error (err, fun_name, arg) -> prerr_string "Unix error : '"; prerr_string fun_name; prerr_string "' failed"; |