From 0a500b73fc9bd6c6752c7bf0079e2305d0040303 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 14 Oct 2016 14:19:40 +0200 Subject: Remove undocumented option. Bug 20193 --- driver/Driver.ml | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) (limited to 'driver/Driver.ml') 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 Control generation of debugging information\n\ \ (=0: none, =1: only-globals, =2: globals + locals\n\ \ without locations, =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; -- cgit