1
0
mirror of https://github.com/luanti-org/luanti.git synced 2025-10-12 16:15:20 +02:00

Fix API site build (#8551)

This commit is contained in:
Paul Ouellette
2019-05-21 13:37:10 -04:00
committed by SmallJoker
parent cfef466d4e
commit 920bd3b16f
3 changed files with 11 additions and 34 deletions

View File

@@ -1,9 +1,7 @@
#!/bin/sh -e
# Patch Pygments and Python-Markdown
PYGMENTS_FILE=$(pip show pygments | awk '/Location/ { print $2 }')/pygments/formatters/html.py
# Patch Python-Markdown
MARKDOWN_FILE=$(pip show markdown | awk '/Location/ { print $2 }')/markdown/extensions/codehilite.py
patch -N -r - $PYGMENTS_FILE code_tag.patch || true
patch -N -r - $MARKDOWN_FILE lua_highlight.patch || true
# Split lua_api.txt on top level headings