From 67f4ae2b702cc95ed7cef67b726e15abbf18e768 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 16 Jul 2021 15:26:03 +0200 Subject: use a more recognizable option name --- driver/Clflags.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'driver/Clflags.ml') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index d01b57f0..085eaa7e 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -116,5 +116,5 @@ let option_profile_arcs = ref false let option_fbranch_probabilities = ref true let option_debug_compcert = ref 0 let option_regpres_threshold = ref 2 -let option_regpres_temp = ref false +let option_regpres_wait_window = ref false let main_function_name = ref "main" -- cgit