aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Driver.ml
diff options
context:
space:
mode:
Diffstat (limited to 'driver/Driver.ml')
-rw-r--r--driver/Driver.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 98e057d4..c68c066a 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -296,7 +296,6 @@ let cmdline_actions =
Exact "-O", Unit (set_all optimization_options);
_Regexp "-O[123]$", Unit (set_all optimization_options);
Exact "-Os", Set option_Osize;
- Exact "-pp-optimizer", String(fun s -> option_pp_optimizer := if (s == "list_scheduler") then 1 else if (s == "cascaded_scheduler") then 2 else 0);
Exact "-fsmall-data", Integer(fun n -> option_small_data := n);
Exact "-fsmall-const", Integer(fun n -> option_small_const := n);
Exact "-ffloat-const-prop", Integer(fun n -> option_ffloatconstprop := n);