diff options
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Driver.ml | 1 |
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); |