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 15063c483..7412c4d4e 100644 --- a/manual/.gitignore +++ b/manual/.gitignore @@ -6,3 +6,4 @@ *.out *.pdf *.toc +*.ok |