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/Driver.ml | |
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/Driver.ml')
-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); |