diff options
Diffstat (limited to 'manual/.gitignore')
| -rw-r--r-- | manual/.gitignore | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/manual/.gitignore b/manual/.gitignore index 8ae9cbde..110f65b1 100644 --- a/manual/.gitignore +++ b/manual/.gitignore @@ -8,4 +8,5 @@ *.toc *.snm *.nav +*.vrb *.ok |