aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Clflags.ml
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-03-15 09:57:03 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-03-15 09:57:03 +0100
commit6803d06880b0ecda94d70549b61998db84160e5b (patch)
tree3bb1bdc8b4d93e39f75e47ef94f763bd9abd05aa /driver/Clflags.ml
parent5e045a7b8c6b834dfec782ecdadae3145a16212e (diff)
parentd0326db1105704e02e2b40facc2a85a267a2b9b5 (diff)
downloadcompcert-kvx-6803d06880b0ecda94d70549b61998db84160e5b.tar.gz
compcert-kvx-6803d06880b0ecda94d70549b61998db84160e5b.zip
Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3
Diffstat (limited to 'driver/Clflags.ml')
-rw-r--r--driver/Clflags.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index a8594be4..901aaa59 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -83,3 +83,4 @@ let option_faddx = ref false
let option_fcoalesce_mem = ref true
let option_fforward_moves = ref true
let option_all_loads_nontrap = ref false
+let option_inline_auto_threshold = ref 0