diff options
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 |