diff options
Diffstat (limited to 'exportclight/Clightgen.ml')
| -rw-r--r-- | exportclight/Clightgen.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml index a5d48a3f..ccdaabc4 100644 --- a/exportclight/Clightgen.ml +++ b/exportclight/Clightgen.ml @@ -47,7 +47,7 @@ let command ?stdout args = if stdout <> None then Unix.close fd_out; match status with | Unix.WEXITED rc -> rc - | Unix.WSIGNALED n | Unix.WSTOPPED n -> + | Unix.WSIGNALED _ | Unix.WSTOPPED _ -> eprintf "Command '%s' killed on a signal.\n" argv.(0); -1 with Unix.Unix_error(err, fn, param) -> eprintf "Error executing '%s': %s: %s %s\n" @@ -186,7 +186,7 @@ let process_c_file sourcename = let explode_comma_option s = match Str.split (Str.regexp ",") s with | [] -> assert false - | hd :: tl -> tl + | _ :: tl -> tl let usage_string = "The CompCert Clight generator @@ -293,4 +293,3 @@ let _ = Builtins.set C2C.builtins; CPragmas.initialize(); parse_cmdline cmdline_actions - |