gbdev/rgbds
1
0
Fork 0
mirror of https://github.com/gbdev/rgbds.git synced 2025-11-24 12:02:08 +00:00
Code Issues Packages Projects Releases Wiki Activity

Get rid of in-repo HTML documentation

Browse Source 
The online documentation is now managed by a CI hook
This commit is contained in:
ISSOtm
2020-09-15 18:39:22 +02:00
parent 131ad9b315
commit 210a4a957a
15 changed files with 2 additions and 5376 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
.github/actions/get-pages.sh vendored
View File

@@ -77,7 +77,7 @@ EOF
if [ $stem = rgbasm.5 ]; then
options+=,toc
fi
mandoc -Thtml -I os=Linux -O$options "${PAGES[$page]##*/}" | src/doc_postproc.awk >> "$1/$2/$page"
mandoc -Thtml -I os=Linux -O$options "${PAGES[$page]##*/}" | .github/actions/doc_postproc.awk >> "$1/$2/$page"
if [ $update_redirects -ne 0 ]; then
cat - >"$1/$page" <<EOF
---