summaryrefslogtreecommitdiffstats
path: root/.gitignore
diff options
context:
space:
mode:
authorThomas Letan <lthms@soap.coffee>2020-02-20 09:25:08 +0100
committerThomas Letan <lthms@soap.coffee>2020-02-20 09:29:54 +0100
commit046606ce1f33c0a2b2955df6ca7dc8b56985d4f0 (patch)
tree5fc76f5dcf71c3e158aa1d5398c092df16674aaa /.gitignore
parentb5ebe89cc8353fd6ad4c6d31022a1c478c699ab2 (diff)
Make cleopatra extensible
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore3
1 files changed, 3 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
index c7d1179..f573e80 100644
--- a/.gitignore
+++ b/.gitignore
@@ -15,6 +15,7 @@ site/style/main.css
site/posts.html
site/news/ColorlessThemes-0.2.html
site/posts/meta/Contents.html
+site/posts/meta/Bootstrap.html
site/posts/meta/Soupault.html
site/posts/Thanks.html
site/posts/meta.html
@@ -26,7 +27,9 @@ site/posts/MiniHTTPServer.html
site/posts/StronglySpecifiedFunctions.html
site/posts/RewritingInCoq.html
site/posts/Ltac101.html
+bootstrap.mk
org.mk
coq.mk
+scripts/tangle-org.el
scripts/export-org.el
# begin generated files