diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-10-14 14:19:40 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-10-14 14:19:40 +0200 |
commit | 0a500b73fc9bd6c6752c7bf0079e2305d0040303 (patch) | |
tree | c15710197018aaa71218072935d7284de7072376 /driver/Driver.ml | |
parent | 7c8bd312880e96f84c15fad18dbffe3fd78397c7 (diff) | |
download | compcert-0a500b73fc9bd6c6752c7bf0079e2305d0040303.tar.gz compcert-0a500b73fc9bd6c6752c7bf0079e2305d0040303.zip |
Remove undocumented option. Bug 20193
Diffstat (limited to 'driver/Driver.ml')
-rw-r--r-- | driver/Driver.ml | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index edee32cf..25d80524 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -255,8 +255,6 @@ let version_string = else "The CompCert C verified compiler, version "^ Version.version ^ "\n" -let gnu_system = Configuration.system <> "diab" - let gnu_debugging_help = " -gdwarf- Generate debug information in DWARF v2 or DWARF v3\n" @@ -266,8 +264,7 @@ let debugging_help = \ -gdepth <n> Control generation of debugging information\n\ \ (<n>=0: none, <n>=1: only-globals, <n>=2: globals + locals\n\ \ without locations, <n>=3: full;)\n" -^ (if gnu_system then gnu_debugging_help else "")^ -" -frename-static Rename static functions and declarations\n" +^ (if gnu_system then gnu_debugging_help else "") let target_help = if Configuration.arch = "arm" then "Target processor options:\n\ @@ -408,8 +405,7 @@ let cmdline_actions = [ Exact "-gdwarf-2", Unit (dwarf_version 2); Exact "-gdwarf-3", Unit (dwarf_version 3);] else []) @ - [ Exact "-frename-static", Set option_rename_static; - Exact "-gdepth", Integer (fun n -> if n = 0 || n <0 then begin + [ Exact "-gdepth", Integer (fun n -> if n = 0 || n <0 then begin option_g := false end else begin option_g := true; |