ci: use emmylua for make types
#2202
Workflow file for this run
This file contains hidden or 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
| name: Main | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: false | |
| on: | |
| pull_request: | |
| branches: | |
| - '*' | |
| push: | |
| branches: | |
| - main | |
| tags: | |
| - 'v*.*.*' | |
| jobs: | |
| release: | |
| name: Release | |
| runs-on: ubuntu-latest | |
| permissions: | |
| contents: write | |
| if: startsWith(github.ref, 'refs/tags/') | |
| steps: | |
| - uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 | |
| - name: Setup Python | |
| uses: actions/setup-python@v5 | |
| with: | |
| python-version: '3.10' | |
| - name: Install requirements | |
| run: | | |
| pip install packaging | |
| - name: Prepare environment | |
| run: | | |
| echo "RELEASE_VERSION=${GITHUB_REF#refs/tags/v}" >> $GITHUB_ENV | |
| echo "TAG=${GITHUB_REF#refs/tags/}" >> $GITHUB_ENV | |
| - name: Generate release notes | |
| run: | | |
| python scripts/release_notes.py > ${{ github.workspace }}-RELEASE_NOTES.md | |
| - name: Publish GitHub release | |
| uses: softprops/action-gh-release@v1 | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| with: | |
| body_path: ${{ github.workspace }}-RELEASE_NOTES.md | |
| prerelease: ${{ contains(env.TAG, 'rc') }} | |
| - name: Sync docs to wiki | |
| shell: bash | |
| run: | | |
| set -euo pipefail | |
| # Clone wiki repo | |
| git clone "https://github.com/${GITHUB_REPOSITORY}.wiki.git" wiki | |
| cd wiki | |
| # Force the correct remote (CI-safe) with token auth | |
| git remote remove origin || true | |
| git remote add origin "https://x-access-token:${{ secrets.GITHUB_TOKEN }}@github.com/${GITHUB_REPOSITORY}.wiki.git" | |
| # Guard: only wiki allowed | |
| REMOTE=$(git remote get-url origin) | |
| case "$REMOTE" in | |
| *".wiki.git") ;; | |
| *) | |
| echo "❌ Refusing to push to non-wiki remote: $REMOTE" | |
| exit 1 | |
| ;; | |
| esac | |
| # CI identity | |
| git config user.name "github-actions" | |
| git config user.email "github-actions@github.com" | |
| # Sync docs -> wiki root | |
| rsync -av --delete --exclude '.git' --exclude '.*' "${GITHUB_WORKSPACE}/docs/" . | |
| # Commit only if changes exist | |
| git add -A | |
| git diff --cached --quiet || git commit -m "Sync docs from main repo (${GITHUB_REF#refs/tags/})" | |
| # Push changes (wiki default branch is often master) | |
| git push origin HEAD:master |