aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Clflags.ml
diff options
context:
space:
mode:
authorDavid Monniaux <David.Monniaux@univ-grenoble-alpes.fr>2021-07-16 15:26:03 +0200
committerDavid Monniaux <David.Monniaux@univ-grenoble-alpes.fr>2021-07-16 15:26:03 +0200
commit67f4ae2b702cc95ed7cef67b726e15abbf18e768 (patch)
tree6a28b2b1c7d6feecb12ce810703b356625356231 /driver/Clflags.ml
parent6121be54b80a55fdadd8b64dfad53357148c9090 (diff)
downloadcompcert-kvx-67f4ae2b702cc95ed7cef67b726e15abbf18e768.tar.gz
compcert-kvx-67f4ae2b702cc95ed7cef67b726e15abbf18e768.zip
use a more recognizable option name
Diffstat (limited to 'driver/Clflags.ml')
-rw-r--r--driver/Clflags.ml2
1 files changed, 1 insertions, 1 deletions
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"