diff options
Diffstat (limited to 'test-suite/dune')
| -rw-r--r-- | test-suite/dune | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/dune b/test-suite/dune index 041c181d66..6ab2988331 100644 --- a/test-suite/dune +++ b/test-suite/dune @@ -20,6 +20,14 @@ ../dev/header.ml ../dev/tools/update-compat.py ../doc/stdlib/index-list.html.template + ; For the misc/printers.sh test + ../dev/incdir_dune + ../dev/base_include + ../dev/inc_ltac_dune + ../dev/include_printers + ../dev/include_dune + ../dev/top_printers.ml + ../dev/vm_printers.ml ; For the changelog test ../config/coq_config.py (source_tree doc/changelog) |