added licence

[faenuccio]

No description provided.

[bryangingechen]

You probably will need to add this back.

[faenuccio]

But it shows up verbatim in the website... sure?
https://leanprover-community.github.io/cite.html

[bryangingechen]

Ah, strange; I could have sworn we needed them when they were added in this commit: 4c628f1

I'm pretty sure they didn't show up then, but I also have no idea what could be causing them to show up literally now.

[grunweg]

Thanks, LGTM (with the build fixed). "bors delegate"

[riccardobrasca]

I don't understand anything about how the website works, but to avoid having the tags in the website Claude suggests to add the lines

        # Strip Jinja2 raw/endraw tags so they don't appear in rendered output
        src = re.sub(r'\{%[-\s]raw\s*[-]?%\}', '', src)
        src = re.sub(r'\{%[-\s]endraw\s*[-]?%\}', '', src)

in make_site.py (in the def get_contents(template):) function.