diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-15 15:07:47 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-15 15:07:47 +0100 |
| commit | 272a5b812b72f4c3e409ccdbeaf3476d95c4b552 (patch) | |
| tree | 6a8d5e75a11860b69522cef3b512b1ef5effb438 /driver/Driver.ml | |
| parent | 2185164c1845c30ebd4118ed5bc8d339b16663a9 (diff) | |
| download | compcert-272a5b812b72f4c3e409ccdbeaf3476d95c4b552.tar.gz compcert-272a5b812b72f4c3e409ccdbeaf3476d95c4b552.zip | |
Deactivate warning 27 and added back removed code.
The code was mostly there for documentation effort. So warning
27 is deactivated again.
Bug 18349
Diffstat (limited to 'driver/Driver.ml')
| -rw-r--r-- | driver/Driver.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index 7b245e6e..16267128 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -58,7 +58,7 @@ let command ?stdout args = if stdout <> None then Unix.close fd_out; match status with | Unix.WEXITED rc -> rc - | Unix.WSIGNALED _ | Unix.WSTOPPED _ -> + | Unix.WSIGNALED n | Unix.WSTOPPED n -> 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" @@ -681,13 +681,13 @@ let cmdline_actions = Exact "-fall", Self (fun _ -> set_all language_support_options); Exact "-fnone", Self (fun _ -> unset_all language_support_options); (* Debugging options *) - Exact "-g", Self (fun _ -> option_g := true; + Exact "-g", Self (fun s -> option_g := true; option_gdwarf := 3); - Exact "-gdwarf-2", Self (fun _ -> option_g:=true; + Exact "-gdwarf-2", Self (fun s -> option_g:=true; option_gdwarf := 2); - Exact "-gdwarf-3", Self (fun _ -> option_g := true; + Exact "-gdwarf-3", Self (fun s -> option_g := true; option_gdwarf := 3); - Exact "-frename-static", Self (fun _ -> option_rename_static:= true); + Exact "-frename-static", Self (fun s -> option_rename_static:= true); Exact "-gdepth", Integer (fun n -> if n = 0 || n <0 then begin option_g := false end else begin |