Skip to content

Fix a bug in version selector of documentation #3290

Fix a bug in version selector of documentation

Fix a bug in version selector of documentation #3290

Workflow file for this run

# This action automatically labels Pull-Requests
# based on files edited and no of lines changed.
name: Size Labeler / Checker
on:
pull_request_target:
types:
- opened
- reopened
- synchronize
- ready_for_review
- review_requested
- edited
jobs:
label-changes:
if: vars.SMALL_THRESHOLD && vars.MODERATE_THRESHOLD && vars.LARGE_THRESHOLD && github.event.pull_request.draft == false
runs-on: ubuntu-latest
permissions:
pull-requests: write
steps:
# checkout the .ci directory of the develop branch of the main repository sagemath/sage
- name: Checkout the main repo
uses: actions/checkout@v4
with:
sparse-checkout: |
.ci
# Check out the pull request repository and mount it at path /<repo_name>
- name: Checkout the pull request repo
uses: actions/checkout@v4
with:
ref: ${{ github.event.pull_request.head.sha }}
fetch-depth: 0
repository: ${{ github.event.pull_request.head.repo.full_name }}
path: ${{ github.event.pull_request.head.repo.name }}
- name: Add labels based on size
run: |
git fetch origin $BASE_REF
chmod a+x .ci/set_labels_by_changes.sh
.ci/set_labels_by_changes.sh
env:
BASE_REF: ${{ github.base_ref }}
PR_MOUNT_DIR: ${{ github.event.pull_request.head.repo.name }}
BASE_SHA: ${{ github.event.pull_request.base.sha }}
PR_HEAD_SHA: ${{ github.event.pull_request.head.sha }}
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
REPOSITORY: ${{ github.repository }}
PR_REPO: ${{ github.event.pull_request.head.repo.name }}
PR_NUMBER: ${{ github.event.pull_request.number}}
SMALL_THRESHOLD: ${{ vars.SMALL_THRESHOLD }}
MODERATE_THRESHOLD: ${{ vars.MODERATE_THRESHOLD }}
LARGE_THRESHOLD: ${{ vars.LARGE_THRESHOLD }}