aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Driver.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2017-03-08 12:18:36 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2017-03-08 12:18:36 +0100
commitde24549f572deb6519be2216ef364b7c80bfdece (patch)
tree9bd5e24ed2a5783c57f05ed5e2e990091ae956d4 /driver/Driver.ml
parent44b63eb13151ca5c3e83ee6a9e7eb6c0049c3758 (diff)
downloadcompcert-de24549f572deb6519be2216ef364b7c80bfdece.tar.gz
compcert-de24549f572deb6519be2216ef364b7c80bfdece.zip
Added missing dltl to dall.
Diffstat (limited to 'driver/Driver.ml')
-rw-r--r--driver/Driver.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml
index b68331a6..48bd9034 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -374,6 +374,7 @@ let cmdline_actions =
option_dclight := true;
option_dcminor := true;
option_drtl := true;
+ option_dltl := true;
option_dalloctrace := true;
option_dmach := true;
option_dasm := true);