diff --git a/tools/ptests/.gitignore b/tools/ptests/.gitignore index 0f6dcce059df79a4688dd572e4e159126ff7e313..0d183328a0be2309eef8d8759cadb39e013c00c7 100644 --- a/tools/ptests/.gitignore +++ b/tools/ptests/.gitignore @@ -1 +1,3 @@ /ptests_config.ml +/tests/cmd/tests/without-test_config/result +/tests/nothing/tests/basic/result/