Commit bc8e2d15 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Gitignore LaTeX temp files.

parent 1b925f41
Pipeline #21025 passed with stage
in 18 minutes and 55 seconds
......@@ -19,3 +19,12 @@ Makefile.coq
  • @robbertkrebbers I am going to revert this; we have a .gitignore in the tex folder for that.

  • Ralf Jung @jung

    mentioned in commit 4f3eb1ac


    mentioned in commit 4f3eb1ac

    Toggle commit list
  • I now see where this comes from---it's because we renamed the docs folder. So the .gitignore didn't cover the left over temp files.

  • Ah. Yes git doesn't know that the folder got renamed, it just moves files around. :/

Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment