summaryrefslogtreecommitdiff
path: root/dune
diff options
context:
space:
mode:
authorThomas Refis <thomas.refis@gmail.com>2018-11-26 16:42:19 +0000
committerThomas Refis <thomas.refis@gmail.com>2018-11-26 16:42:19 +0000
commitf86d10aebdd62ba3ad4412a500e067efa65b541c (patch)
tree0b61f10c44fbe5fd76e3ca78aca88a5260da18ad /dune
parent6dc171e38779d232fc429ebf03432743bd14f2de (diff)
downloadocaml-f86d10aebdd62ba3ad4412a500e067efa65b541c.tar.gz
update dune file
Diffstat (limited to 'dune')
-rw-r--r--dune3
1 files changed, 2 insertions, 1 deletions
diff --git a/dune b/dune
index f51dcd3b33..f5c7fc3ffa 100644
--- a/dune
+++ b/dune
@@ -55,7 +55,8 @@
typedtree printtyped ctype printtyp includeclass mtype envaux includecore
typedtreeIter typedtreeMap tast_mapper cmt_format untypeast includemod
typetexp printpat parmatch stypes typedecl typeopt rec_check typecore
- typeclass typemod
+ typeclass typemod typedecl_variance typedecl_properties typedecl_immediacy
+ typedecl_unboxed
; manual update: mli only files
annot outcometree