aboutsummaryrefslogtreecommitdiffstats
path: root/.gitignore
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2022-03-03 18:34:12 +0000
committerYann Herklotz <git@yannherklotz.com>2022-03-03 18:34:12 +0000
commitdff5106bec7062701c3dc4d548aea081803e35a5 (patch)
tree55df778bed63b919181d00f4aa4f8a310ab633ff /.gitignore
parentc34b7ac31427861e066ea7f9fc7d964598aa4ed4 (diff)
downloadbiteq-dff5106bec7062701c3dc4d548aea081803e35a5.tar.gz
biteq-dff5106bec7062701c3dc4d548aea081803e35a5.zip
Remove built files
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore4
1 files changed, 4 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
index 94634d9..62d1d85 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,2 +1,6 @@
*~
*.coq.all*
+
+*.vo
+*.vos
+*.vok