summaryrefslogtreecommitdiffstats
path: root/.gitignore
diff options
context:
space:
mode:
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