diff options
| author | Thomas Letan <lthms@soap.coffee> | 2020-02-05 21:47:57 +0100 |
|---|---|---|
| committer | Thomas Letan <lthms@soap.coffee> | 2020-02-05 21:47:57 +0100 |
| commit | a69a2cc1ffe4a0642a78468fe47b67e1c4fb2374 (patch) | |
| tree | 046c796b963aa00f3be3d876d8b7b20ffc4081b4 /.gitignore | |
| parent | Publish a new article (diff) | |
Keep the list of html files to ignore up-to-date when building
Diffstat (limited to '.gitignore')
| -rw-r--r-- | .gitignore | 13 |
1 files changed, 12 insertions, 1 deletions
@@ -5,4 +5,15 @@ build/ *.vo .*.aux *.glob -*.html~
\ No newline at end of file +*.html~ + +# begin generated files +site/posts/monad-transformers.html +site/posts/lisp-journey-getting-started.html +site/posts/extensible-type-safe-error-handling.html +site/posts/Ltac101.html +site/posts/RewritingInCoq.html +site/posts/StronglySpecifiedFunctionsProgram.html +site/posts/MiniHTTPServer.html +site/posts/StronglySpecifiedFunctions.html +# begin generated files |