summaryrefslogtreecommitdiffstats
path: root/.gitignore
diff options
context:
space:
mode:
authorThomas Letan <lthms@soap.coffee>2020-02-15 00:41:49 +0100
committerThomas Letan <lthms@soap.coffee>2020-02-15 00:44:31 +0100
commitc1493078e3ff16db8175a0da0439ca0aeb3f5422 (patch)
tree762b95dc42142e508c3b8e7327c87f831f1003a8 /.gitignore
parentFix spelling error (diff)
Self hosting of Fira Sans and various small fixes
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore10
1 files changed, 5 insertions, 5 deletions
diff --git a/.gitignore b/.gitignore
index fe3275d..9d9e78e 100644
--- a/.gitignore
+++ b/.gitignore
@@ -8,13 +8,13 @@ build/
*.html~
# begin generated files
-site/posts.html
-site/posts/DiscoveringCommonLisp.html
site/posts/ExtensibleTypeSafeErrorHandling.html
+site/posts/DiscoveringCommonLisp.html
site/posts/MonadTransformers.html
-site/posts/StronglySpecifiedFunctionsProgram.html
-site/posts/MiniHTTPServer.html
-site/posts/StronglySpecifiedFunctions.html
+site/posts.html
site/posts/RewritingInCoq.html
+site/posts/StronglySpecifiedFunctions.html
site/posts/Ltac101.html
+site/posts/StronglySpecifiedFunctionsProgram.html
+site/posts/MiniHTTPServer.html
# begin generated files