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 | |
| parent | 7c8bd312880e96f84c15fad18dbffe3fd78397c7 (diff) | |
| download | compcert-0a500b73fc9bd6c6752c7bf0079e2305d0040303.tar.gz compcert-0a500b73fc9bd6c6752c7bf0079e2305d0040303.zip | |
Remove undocumented option. Bug 20193
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Clflags.ml | 1 | ||||
| -rw-r--r-- | driver/Driver.ml | 8 | ||||
| -rw-r--r-- | driver/Optionsprinter.ml | 1 |
3 files changed, 2 insertions, 8 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 6a695aa4..f8c38a54 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -60,6 +60,5 @@ let option_small_data = then 8 else 0) let option_small_const = ref (!option_small_data) let option_timings = ref false -let option_rename_static = ref false let stdlib_path = ref Configuration.stdlib_path let use_standard_headers = ref Configuration.has_standard_headers 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; diff --git a/driver/Optionsprinter.ml b/driver/Optionsprinter.ml index 9dce8592..00b5f5ec 100644 --- a/driver/Optionsprinter.ml +++ b/driver/Optionsprinter.ml @@ -64,7 +64,6 @@ let print_clflags oc = p_jmember oc "small_data" p_jint !option_small_data; p_jmember oc "small_data" p_jint !option_small_const; p_jmember oc "timings" p_jbool !option_timings; - p_jmember oc "rename_static" p_jbool !option_rename_static; fprintf oc "\n}" let print_struct_passing_style oc = function |