.github/workflows/whitespace.yml

   1 name: Whitespace
   2
   3 on:
   4   pull_request:
   5   push:
   6     branches: ["master"]
   7
   8 jobs:
   9   whitespace:
  10     defaults:
  11       run:
  12         shell: bash
  13     runs-on: ubuntu-latest
  14
  15     steps:
  16
  17     - uses: actions/checkout@v4
  18
  19     - run: |
  20         # no longer using the action because apparently we're supposed to use the Makefile here
  21         wget -q https://github.com/agda/fix-whitespace/releases/download/v0.1/fix-whitespace-0.1-linux.binary
  22         mkdir -p "$HOME/.local/bin"
  23         mv fix-whitespace-0.1-linux.binary "$HOME/.local/bin/fix-whitespace"
  24         chmod +x "$HOME/.local/bin/fix-whitespace"
  25         echo "$HOME/.local/bin" >> $GITHUB_PATH
  26
  27     - run: make whitespace