Add .glob to gitignore

logsem · Nov 24, 2020 · 118c366 · 118c366
1 parent 3c0e7d2
commit 118c366
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/.gitignore b/.gitignore
@@ -12,3 +12,4 @@ Makefile.coq.conf
 *.vok
 *.vos
 .lia.cache
+/SimpleLang/*.glob