Store receiver in any_operation_state
to avoid dynamic allocation for receiver
#3526
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
# Copyright (c) 2023 ETH Zurich | |
# | |
# SPDX-License-Identifier: BSL-1.0 | |
# Distributed under the Boost Software License, Version 1.0. (See accompanying | |
# file LICENSE_1_0.txt or copy at http://www.boost.org/LICENSE_1_0.txt) | |
name: Documentation | |
on: | |
merge_group: | |
pull_request: | |
branches: | |
# Development and release branches | |
- main | |
- release** | |
push: | |
branches: | |
# Development and release branches | |
- main | |
- release** | |
jobs: | |
build: | |
name: github/documentation/build | |
runs-on: ubuntu-24.04 | |
steps: | |
- uses: actions/checkout@v4 | |
- name: Install sphinx and a theme | |
run: | | |
sudo apt update | |
sudo apt install \ | |
--allow-downgrades \ | |
--allow-remove-essential \ | |
--allow-change-held-packages \ | |
doxygen python3 python3-pip ripgrep | |
pip install --requirement $PWD/docs/requirements.txt | |
- name: Check that docstrings don't use @command | |
run: | | |
./scripts/check_doxygen_commands.sh $PWD | |
- name: Build documentation | |
run: | | |
export PIKA_DOCS_DOXYGEN_OUTPUT_DIRECTORY=$PWD/build/doxygen | |
export PIKA_DOCS_DOXYGEN_INPUT_ROOT=$PWD | |
mkdir -p $PIKA_DOCS_DOXYGEN_OUTPUT_DIRECTORY | |
doxygen docs/Doxyfile | |
sphinx-build -W -a -b html docs $PWD/build/docs | |
- name: Upload HTML output as artifact | |
uses: actions/upload-pages-artifact@v3 | |
with: | |
path: build/docs | |
deploy: | |
needs: build | |
name: github/documentation/deploy | |
runs-on: ubuntu-24.04 | |
if: github.ref == 'refs/heads/main' && github.repository == 'pika-org/pika' | |
permissions: | |
contents: read | |
pages: write | |
id-token: write | |
concurrency: | |
group: "pages" | |
cancel-in-progress: false | |
environment: | |
name: github-pages | |
url: ${{ steps.deployment.outputs.page_url }} | |
steps: | |
- name: Deploy documentation to GitHub Pages | |
uses: actions/deploy-pages@v4 | |
id: deployment |