(Build & Lint & Wiki).yaml: Make sure all CI scripts run on push for #26
This file contains 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: Wiki | |
| on: | |
| push: | |
| branches: main | |
| paths: [wiki/**, .github/workflows/Wiki.yaml] | |
| pull_request: | |
| branches: main | |
| paths: [wiki/**, .github/workflows/Wiki.yaml] | |
| permissions: | |
| contents: write | |
| jobs: | |
| check_directories: | |
| name: "Audit changes" | |
| runs-on: ubuntu-latest | |
| if: github.event_name == 'pull_request' | |
| steps: | |
| - uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 | |
| - name: "No new directories in ./wiki/" | |
| run: | | |
| if git diff --name-only --diff-filter=A origin/main... | grep -q '^wiki/.*/'; then | |
| echo "New directory detected in wiki folder. This is not allowed." | |
| exit 1 | |
| fi | |
| - name: "No manually added disclaimers" | |
| run: | | |
| notice='Warning: Wiki should not be edited directly' | |
| bad_files=$(grep -rl "$notice" wiki || true) | |
| if [ -n "$bad_files" ]; then | |
| echo "Edit disclaimers are automatically prepended. Please remove those manually added. Bad files:" | |
| echo "$bad_files" | |
| exit 1 | |
| fi | |
| - name: "Windows-friendly file names" | |
| run: | | |
| bad_file_names=$(find wiki -type f -name "*[\\/:*?\"<>|]*") | |
| if [ -n "$bad_file_names" ]; then | |
| echo "Windows-friendly file names must not contain any of \"\\/:*?\"<>|\". Bad files:" | |
| echo "$bad_file_names" | |
| exit 1 | |
| fi | |
| wiki: | |
| name: "Publish changes" | |
| runs-on: ubuntu-latest | |
| if: github.event_name == 'push' && github.ref == 'refs/heads/main' | |
| steps: | |
| - uses: actions/checkout@v4 | |
| with: # Fetch enough history to resolve HEAD^ -- https://github.com/actions/checkout?tab=readme-ov-file#checkout-head | |
| fetch-depth: 2 | |
| - name: "Configure git client" | |
| run: | | |
| git config --global user.name "${{ secrets.BOT_NAME }}" | |
| git config --global user.email "${{ secrets.BOT_EMAIL }}" | |
| - name: "Prepend wiki edit warnings" | |
| run: | | |
| notice='_Warning: Wiki should not be edited directly. Edit the files in the ./wiki/ folder instead and make a PR._' | |
| for file in wiki/*.md; do | |
| [ "$(basename "$file")" = "_Sidebar.md" ] && continue | |
| sed -i '1s|^|'"$notice"'\n\n|' "$file" | |
| done | |
| - name: "Clone .wiki repository" | |
| run: | | |
| git clone https://x-access-token:${{ secrets.BOT_TOKEN }}@github.com/${{ github.repository }}.wiki.git | |
| - name: "Update ~.wiki.git contents" | |
| run: | | |
| rsync -av --delete --exclude '.git' wiki/ ${GITHUB_REPOSITORY##*/}.wiki/ | |
| - name: "Commit and push changes" | |
| run: | | |
| cd ${GITHUB_REPOSITORY##*/}.wiki | |
| git add . | |
| if [ -n "$(git status --porcelain)" ]; then | |
| git commit -m "Update wiki content at ${{ github.sha }}" | |
| git push origin master | |
| else | |
| echo "No changes to commit" | |
| fi |