diff --git a/tools/.gitignore b/tools/.gitignore new file mode 100644 index 0000000..20926dd --- /dev/null +++ b/tools/.gitignore @@ -0,0 +1 @@ +/owl/