diff --git a/src/kernel_internals/parsing/tests/dune b/src/kernel_internals/parsing/tests/dune new file mode 100644 index 0000000000000000000000000000000000000000..ff757cb8ca298349f7475c85a739f5eab4250b24 --- /dev/null +++ b/src/kernel_internals/parsing/tests/dune @@ -0,0 +1 @@ +(include_subdirs no)