diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml deleted file mode 100644 index 6f7a767..0000000 --- a/.github/workflows/release.yml +++ /dev/null @@ -1,37 +0,0 @@ -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 }} \ No newline at end of file