diff options
Diffstat (limited to '.github')
| -rw-r--r-- | .github/workflows/doc.yml | 14 |
1 files changed, 14 insertions, 0 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 }} |