CI: fix the document action for divergent branches.

This was never intended to merge anything.
This commit is contained in:
Catherine 2023-05-22 20:25:21 +00:00
parent 7d99981d57
commit 8af90620c0

View file

@ -60,9 +60,9 @@ jobs:
uses: actions/checkout@v3
with:
fetch-depth: 0
- name: Pull tags from upstream repository
- name: Fetch tags from upstream repository
run: |
git pull --tags https://github.com/amaranth-lang/amaranth.git
git fetch --tags https://github.com/amaranth-lang/amaranth.git
- name: Set up Python
uses: actions/setup-python@v4
with: