diff --git a/.github/workflows/build_doc.yml b/.github/workflows/build_doc.yml index cf65f46fcb9..705ead0028c 100644 --- a/.github/workflows/build_doc.yml +++ b/.github/workflows/build_doc.yml @@ -214,7 +214,6 @@ jobs: done cat index.html | grep -F "$(echo */ | tr ' ' '\n')" > index.html git add ${PR_NUMBER}/$ROUND index.html && git commit -q --amend -m "sole commit" && git push -q -f -u origin master - exit $exit_code else echo "DoxygenError=This round already exists. Overwrite it with /force-build." >> $GITHUB_OUTPUT exit 1