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/Optionsprinter.ml | |
| parent | 7c8bd312880e96f84c15fad18dbffe3fd78397c7 (diff) | |
| download | compcert-0a500b73fc9bd6c6752c7bf0079e2305d0040303.tar.gz compcert-0a500b73fc9bd6c6752c7bf0079e2305d0040303.zip | |
Remove undocumented option. Bug 20193
Diffstat (limited to 'driver/Optionsprinter.ml')
| -rw-r--r-- | driver/Optionsprinter.ml | 1 |
1 files changed, 0 insertions, 1 deletions
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 |