diff --git a/developer-doc/.gitignore b/developer-doc/.gitignore index 975bc156cc..42e5b08651 100644 --- a/developer-doc/.gitignore +++ b/developer-doc/.gitignore @@ -5,5 +5,6 @@ /*PP.txt /links-to-user-manual.md /plumedcheck.md -/coverage +/coverage*/ +/coverage*