diff options
Diffstat (limited to 'doc/manual/.gitignore')
| -rw-r--r-- | doc/manual/.gitignore | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/manual/.gitignore b/doc/manual/.gitignore index bc9331596..c4decec05 100644 --- a/doc/manual/.gitignore +++ b/doc/manual/.gitignore @@ -2,3 +2,5 @@ screenshots/*.pdf verify_bv21_errors.xml verify_errors.xml verify_warnings.xml +verify_ok.xml + |