diff --git a/docs/makedocs b/docs/makedocs index 792f9f791..5eb43bca2 100755 --- a/docs/makedocs +++ b/docs/makedocs @@ -6,6 +6,11 @@ report_failure () exit 1 } +htmlify_python_file () +{ + pygmentize -f html -O full,style=vs $1 > $1.html +} + htmlify_cmake () { echo "