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/Optionsprinter.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'driver/Optionsprinter.ml') 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 -- cgit