1 files changed, 1 insertions, 0 deletions

diff --git a/.gitignore b/.gitignore
index 5358ee05..99ec0c72 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,6 +1,7 @@
 # Object files, in general
 **.bin
 **.out
+**.tok
 *.vo
 *.glob
 *.o