diff --git a/src/plugins/instantiate/.gitignore b/src/plugins/instantiate/.gitignore index b18adc61b4fbcc6e775225047b0a86a8a8a8659d..cf191ced79913e05a88f7328899d77f503fc77f4 100644 --- a/src/plugins/instantiate/.gitignore +++ b/src/plugins/instantiate/.gitignore @@ -1,4 +1,4 @@ /configure /Makefile -/tests/**/dune +/tests/*/oracle/dune /tests/*/result