diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-10 19:17:24 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-10 19:17:24 +0100 |
| commit | 7247e4bb85d50834983bc71e6415fe1bf065aa46 (patch) | |
| tree | b5d1de65396c1bd08e44c282ffd59ab0ba876e8f /exportclight/Clightgen.ml | |
| parent | 7a8a7b225321b70d7a4a2ca5f6e1ba811bd378ab (diff) | |
| download | compcert-7247e4bb85d50834983bc71e6415fe1bf065aa46.tar.gz compcert-7247e4bb85d50834983bc71e6415fe1bf065aa46.zip | |
Cleanup of Clightgen code.
Removed unused code and code generating warnings.
Bug 18394
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 - |