{{ cannot be used in markdown files

[bryangingechen]

We're telling staticjinja that every .md file is a jinja2 template, so if one of them contains {{ (e.g. when talking about "weakly implicit" arguments in Lean, (usually written ⦃ in unicode)), jinja2 will be unable to parse the file and then complain:

jinja2.exceptions.TemplateSyntaxError: unexpected char 'XX' at YY

This came up when testing templates/latex.md in #165.

[robertylewis]

Are we using this feature at all? It looks like all our jinja2 templates are .html files, but I'm not sure. Also I have no idea how to disable this processing on markdown files. So this isn't a very helpful question...

[bryangingechen]

I agree that we're not actually using the markdown files as templates, and I tried to figure out how to disable the checking but it seemed like it would require a bigger refactor, so I didn't dig too hard.

I did a search just now and we do actually have {{ in ci.md inside a yaml code block:

          repo: ${{ github.repository }}
          access-token: ${{ secrets.GITHUB_TOKEN }}

and contribute/doc.md inside a Lean code block:

| binder_info.strict_implicit := ("{{", "}}")

So this may be less of a big deal than I thought. In the example that was breaking, {{ was in one of the LaTeX tests that wasn't in a code block and jinja complained, so I changed it to { {.