aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Driver.ml
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-05-11 21:54:18 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-05-11 21:54:18 +0200
commit66ee59d3dc8a861b468cfaf0ff46fc71dfb8fec2 (patch)
treece2b6bb7c0dc8d00eac6adf7f66388528bfe650a /driver/Driver.ml
parent17a8d91a82f67d7f62f8cbad41ba76a4b0b82a30 (diff)
downloadcompcert-kvx-66ee59d3dc8a861b468cfaf0ff46fc71dfb8fec2.tar.gz
compcert-kvx-66ee59d3dc8a861b468cfaf0ff46fc71dfb8fec2.zip
option -faddx (off by default until questions cleared)
Diffstat (limited to 'driver/Driver.ml')
-rw-r--r--driver/Driver.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml
index cfafcaa3..74e7ae77 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -375,7 +375,8 @@ let cmdline_actions =
@ f_opt "globaladdrtmp" option_fglobaladdrtmp
@ f_opt "globaladdroffset" option_fglobaladdroffset
@ f_opt "xsaddr" option_fxsaddr
- @ f_opt "coalesce-mem" option_coalesce_mem
+ @ f_opt "addx" option_faddx
+ @ f_opt "coalesce-mem" option_fcoalesce_mem
(* Code generation options *)
@ f_opt "fpu" option_ffpu
@ f_opt "sse" option_ffpu (* backward compatibility *)