summaryrefslogtreecommitdiffstats
path: root/.gitignore
diff options
context:
space:
mode:
authorThomas Letan <lthms@soap.coffee>2020-02-14 08:06:52 +0100
committerThomas Letan <lthms@soap.coffee>2020-02-14 08:06:52 +0100
commit707ccc2e782b359725308ebd8cbcc3f904a1b0d9 (patch)
tree3766533c63b055ae1e45f9fbe0842125bc8169b6 /.gitignore
parentRename org posts (diff)
Provide an index page for write-ups with more value
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore7
1 files changed, 4 insertions, 3 deletions
diff --git a/.gitignore b/.gitignore
index 6c3c797..fe3275d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -8,12 +8,13 @@ build/
*.html~
# begin generated files
+site/posts.html
+site/posts/DiscoveringCommonLisp.html
site/posts/ExtensibleTypeSafeErrorHandling.html
site/posts/MonadTransformers.html
-site/posts/DiscoveringCommonLisp.html
-site/posts/Ltac101.html
-site/posts/RewritingInCoq.html
site/posts/StronglySpecifiedFunctionsProgram.html
site/posts/MiniHTTPServer.html
site/posts/StronglySpecifiedFunctions.html
+site/posts/RewritingInCoq.html
+site/posts/Ltac101.html
# begin generated files