From db48853f3dfabb8ece26ccbdb08d4fae30a09204 Mon Sep 17 00:00:00 2001 From: Max Horn Date: Mon, 8 Sep 2025 00:53:43 +0200 Subject: [PATCH] Set up release workflow For making a release from the GitHub web interface. Usage instructions at . --- .github/workflows/release.yml | 37 +++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) create mode 100644 .github/workflows/release.yml diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml new file mode 100644 index 0000000..817e909 --- /dev/null +++ b/.github/workflows/release.yml @@ -0,0 +1,37 @@ +name: Release + +on: + workflow_dispatch: + inputs: + dry-run: + description: "Only create an archive containing the release instead of publishing it on GitHub" + type: boolean + required: false + default: false + force: + description: "Allow overwriting an existing release, or making a release with an incorrect date" + type: boolean + required: false + default: false + +permissions: write-all + +jobs: + release: + name: "Release the GAP package" + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v5 + - uses: gap-actions/setup-gap@v2 + with: + GAP_PKGS_TO_BUILD: json + - uses: gap-actions/build-pkg-docs@v1 + with: + use-latex: true + - uses: gap-actions/release-pkg@v1 + with: + dry-run: ${{ inputs.dry-run }} + force: ${{ inputs.force }} + - uses: gap-actions/update-gh-pages@v1 + if: ${{ !inputs.dry-run }}