diff options
Diffstat (limited to 'docs')
-rwxr-xr-x | docs/make.sh | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/docs/make.sh b/docs/make.sh index 544d1f3..76a30af 100755 --- a/docs/make.sh +++ b/docs/make.sh @@ -1,7 +1,17 @@ #! /bin/bash PAGES=(ethernet features wireless) +make_page() { + echo '<html><body>' + grep -v '^%' $1 | markdown -x def_list -x headerid /dev/stdin + echo '</body></html>' +} + for page in ${PAGES[@]}; do - rm ${page}.html - pandoc -s --toc -w html --email-obfuscation=javascript -c header.css -o ${page}.html $page + rm -f ${page}.html + if [ -f /usr/bin/pandoc ]; then + pandoc -s --toc -w html --email-obfuscation=javascript -c header.css -o ${page}.html $page + else + make_page $page > ${page}.html + fi done |