Skip to content

feat(Analysis/PolarCoord): add versions for Lebesgue integral #1821

feat(Analysis/PolarCoord): add versions for Lebesgue integral

feat(Analysis/PolarCoord): add versions for Lebesgue integral #1821

name: Autolabel PRs
on:
pull_request:
types: [opened]
push:
paths:
- scripts/autolabel.lean
- .github/workflows/add_label_from_diff.yaml
jobs:
add_topic_label:
name: Add topic label
runs-on: ubuntu-latest
# Don't run on forks, where we wouldn't have permissions to add the label anyway.
if: github.repository == 'leanprover-community/mathlib4'
permissions:
issues: write
checks: write
pull-requests: write
contents: read
steps:
- name: Checkout code
uses: actions/checkout@v4
with:
fetch-depth: 0
- name: install elan
run: |
set -o pipefail
curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
./elan-init -y --default-toolchain none
echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
- name: lake exe autolabel
run: |
# the checkout dance, to avoid a detached head
git checkout master
git checkout -
lake exe autolabel "$NUMBER"
env:
GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
GH_REPO: ${{ github.repository }}
NUMBER: ${{ github.event.number }}