aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Clflags.ml
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-10-22 13:38:45 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-10-22 13:38:45 +0200
commit4764b4e2cf2fedb6165e4bf31d549f1df4e4a347 (patch)
tree8bc92939381b8e48d75408b6d69bd884eb25a4c5 /driver/Clflags.ml
parent1740571e67f4c9384aea706132b534411d24b36c (diff)
downloadcompcert-kvx-4764b4e2cf2fedb6165e4bf31d549f1df4e4a347.tar.gz
compcert-kvx-4764b4e2cf2fedb6165e4bf31d549f1df4e4a347.zip
-mtune=
Diffstat (limited to 'driver/Clflags.ml')
-rw-r--r--driver/Clflags.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index d5f3aca5..a817b56a 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -42,6 +42,8 @@ let option_funrollsingle = ref 0 (* unroll a single iteration of innermost loops
let option_funrollbody = ref 0 (* unroll the body of innermost loops of size n *)
(* Scheduling *)
+let option_mtune = ref ""
+
let option_fprepass = ref false
let option_fprepass_sched = ref "list"