diff options
author | UnavailableDev <69792062+UnavailableDev@users.noreply.github.com> | 2023-05-22 09:52:24 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2023-05-22 09:52:24 +0200 |
commit | 9540b10df8b89eee39dc2eccb26286baa7626891 (patch) | |
tree | 372cdf114a176e8d818e96468f9c05978a78fcf5 /doc/.gitignore | |
parent | ac1884bec264d08dc5cc58d1cda24e20734c9205 (diff) | |
parent | 5e2cfc62ca7d724e6f9e2a4081e0cb5f948ffc71 (diff) |
Merge branch 'lonkaars:master' into master
Diffstat (limited to 'doc/.gitignore')
-rw-r--r-- | doc/.gitignore | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/.gitignore b/doc/.gitignore index 25dcb3b..e5139ef 100644 --- a/doc/.gitignore +++ b/doc/.gitignore @@ -12,6 +12,8 @@ *.toc *.synctex(busy) *.md.tex +*.lof +*.lot # ignore output files *.pdf |