aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelib.ml
diff options
context:
space:
mode:
authorMaxime Dénès2016-06-28 13:55:20 +0200
committerMaxime Dénès2016-06-28 13:57:33 +0200
commit0e07e69dae3f3f4a99f824533f54a3991aacac6a (patch)
treef2022d27c1742b3f3e99d76204a51860b6bc6ad5 /kernel/nativelib.ml
parenteb72574e1b526827706ee06206eb4a9626af3236 (diff)
Revert "A new infrastructure for warnings."
This reverts commit 925d258d7d03674c601a1f3832122b3b4b1bc9b0. I forgot that Jenkins gave me a spurious success when trying to build this PR. There are a few rough edges to fix, so reverting meanwhile. The Jenkins issue has been fixed by Matej. Sorry for the noise.
Diffstat (limited to 'kernel/nativelib.ml')
-rw-r--r--kernel/nativelib.ml20
1 files changed, 7 insertions, 13 deletions
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index d4a67b3999..5b92e9554f 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -55,15 +55,6 @@ let write_ml_code fn ?(header=[]) code =
List.iter (pp_global fmt) (header@code);
close_out ch_out
-let warn_native_compiler_failed =
- let print = function
- | Inl (Unix.WEXITED n) -> Pp.(strbrk "Native compiler exited with status" ++ str" " ++ int n)
- | Inl (Unix.WSIGNALED n) -> Pp.(strbrk "Native compiler killed by signal" ++ str" " ++ int n)
- | Inl (Unix.WSTOPPED n) -> Pp.(strbrk "Native compiler stopped by signal" ++ str" " ++ int n)
- | Inr e -> Pp.(strbrk "Native compiler failed with error: " ++ strbrk (Unix.error_message e))
- in
- CWarnings.create ~name:"native-compiler-failed" ~category:"native-compiler" print
-
let call_compiler ml_filename =
let load_path = !get_load_paths () in
let load_path = List.map (fun dn -> dn / output_dir) load_path in
@@ -87,12 +78,15 @@ let call_compiler ml_filename =
let res = CUnix.sys_command (ocamlfind ()) args in
let res = match res with
| Unix.WEXITED 0 -> true
- | Unix.WEXITED n | Unix.WSIGNALED n | Unix.WSTOPPED n ->
- warn_native_compiler_failed (Inl res); false
- in
+ | Unix.WEXITED n ->
+ Feedback.msg_warning Pp.(str "command exited with status " ++ int n); false
+ | Unix.WSIGNALED n ->
+ Feedback.msg_warning Pp.(str "command killed by signal " ++ int n); false
+ | Unix.WSTOPPED n ->
+ Feedback.msg_warning Pp.(str "command stopped by signal " ++ int n); false in
res, link_filename
with Unix.Unix_error (e,_,_) ->
- warn_native_compiler_failed (Inr e);
+ Feedback.msg_warning Pp.(str (Unix.error_message e));
false, link_filename
let compile fn code =