diff --git a/collects/tests/mred/.gitignore b/collects/tests/mred/.gitignore new file mode 100644 index 00000000..ee4173f0 --- /dev/null +++ b/collects/tests/mred/.gitignore @@ -0,0 +1 @@ +/tmp*