diff options
-rw-r--r-- | .github/workflows/doc.yml | 14 | ||||
-rw-r--r-- | doc/conf.py | 4 |
2 files changed, 15 insertions, 3 deletions
diff --git a/.github/workflows/doc.yml b/.github/workflows/doc.yml index fe5d0cc18..6d904b01f 100644 --- a/.github/workflows/doc.yml +++ b/.github/workflows/doc.yml @@ -15,8 +15,22 @@ jobs: docker build -t ghdl/doc - <<-EOF FROM ghdl/vunit:llvm ENV PYTHONPATH=/src/python + RUN apt update -qq && apt install -y gnat-gps EOF + - name: Run gnatdoc + run: | + cat > run.sh <<-EOF + #!/usr/bin/env sh + ./configure + make + gnatdoc -P./ghdl + mkdir public + mv gnatdoc public + EOF + chmod +x run.sh + docker run --rm -v $(pwd):/src -w /src ghdl/doc ./run.sh + - uses: buildthedocs/btd@v0 with: token: ${{ github.token }} diff --git a/doc/conf.py b/doc/conf.py index dff335e4d..ced332c9a 100644 --- a/doc/conf.py +++ b/doc/conf.py @@ -113,10 +113,8 @@ if ctx.is_file(): html_theme_path = ["."] html_theme = "_theme" -# Add any paths that contain custom static files (such as style sheets) here, -# relative to this directory. They are copied after the builtin static files, -# so a file named "default.css" will overwrite the builtin "default.css". html_static_path = ['_static'] +html_extra_path = [str(Path(__file__).resolve().parent.parent / 'public')] # Output file base name for HTML help builder. htmlhelp_basename = 'GHDLdoc' |