diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-12-02 17:22:49 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-12-02 17:22:49 +0100 |
| commit | e62820c430e52fa72edd6f1c21bd867eb0f3c467 (patch) | |
| tree | 6ae9c86fc9e51d2f3ca128c0c0c96d3fda0d2a84 /driver | |
| parent | 56690956f52349c3398b3de6f8ec3987501e9034 (diff) | |
| download | compcert-e62820c430e52fa72edd6f1c21bd867eb0f3c467.tar.gz compcert-e62820c430e52fa72edd6f1c21bd867eb0f3c467.zip | |
Renamed the printer module for the Abbreviations and deactivated adding the -g option to the assembler.
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Driver.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index fec87420..6ba30d74 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -499,7 +499,7 @@ 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 s -> option_g := true; push_linker_arg s); + Exact "-g", Self (fun s -> option_g := true); (* Code generation options -- more below *) Exact "-O0", Self (fun _ -> unset_all optimization_options); Exact "-O", Self (fun _ -> set_all optimization_options); |