Fix agda support #14
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
| --- | |
| # Mega-Linter GitHub Action configuration file | |
| # More info at https://github.com/nvuillam/mega-linter#readme | |
| name: Mega-Linter | |
| on: | |
| # Trigger mega-linter at every push. Action will also be visible from Pull Requests to master | |
| push: # Comment this line to trigger action only on pull-requests (not recommended if you don't pay for GH Actions) | |
| pull_request: | |
| branches: [master] | |
| env: #Uncomment to activate variables below | |
| # Apply linter fixes configuration | |
| APPLY_FIXES: all # Uncomment to apply fixes provided by linters. You can also specify the list of fixing linters | |
| APPLY_FIXES_EVENT: pull_request # Decide which event triggers application of fixes in a commit or a PR (pull_request (default), push, all) | |
| APPLY_FIXES_MODE: commit # If APPLY_FIXES is used, defines if the fixes are directly committed (commit) or posted in a PR (pull_request) | |
| jobs: | |
| build: | |
| name: Mega-Linter | |
| runs-on: ubuntu-latest | |
| steps: | |
| # Git Checkout | |
| - name: Checkout Code | |
| uses: actions/checkout@v2 | |
| with: | |
| token: ${{ secrets.PAT || secrets.GITHUB_TOKEN }} | |
| fetch-depth: 0 | |
| # Mega-Linter | |
| - name: Mega-Linter | |
| uses: nvuillam/mega-linter@insiders | |
| env: | |
| # All available variables are described in documentation | |
| # https://github.com/nvuillam/mega-linter#configuration | |
| VALIDATE_ALL_CODEBASE: ${{ github.event_name == 'push' && github.ref == 'refs/heads/master' }} # Validates all source when push on master, else just the git diff with master. Override with true if you always want to lint all sources | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| # DISABLE: COPYPASTE,SPELL | |
| FILTER_REGEX_EXCLUDE: (/github/workspace/spec/testfiles/) | |
| # Upload Mega-Linter artifacts. They will be available on Github action page "Artifacts" section | |
| - name: Archive production artifacts | |
| if: ${{ success() }} || ${{ failure() }} | |
| uses: actions/upload-artifact@v2 | |
| with: | |
| name: Mega-Linter reports | |
| path: | | |
| report | |
| mega-linter.log | |
| # This step will evaluate the repo status and report the change | |
| - name: Check if there are changes | |
| id: changes | |
| if: ${{ success() }} || ${{ failure() }} | |
| uses: UnicornGlobal/has-changes-action@v1.0.11 | |
| # Create pull request if applicable | |
| - name: Create Pull Request with applied fixes | |
| if: steps.changes.outputs.changed == 1 && (env.APPLY_FIXES_EVENT == 'all' || env.APPLY_FIXES_EVENT == github.event_name) && env.APPLY_FIXES_MODE == 'pull_request' | |
| uses: peter-evans/create-pull-request@v3 | |
| with: | |
| token: ${{ secrets.PAT || secrets.GITHUB_TOKEN }} | |
| commit-message: "[Mega-Linter] Apply linters automatic fixes" | |
| title: "[Mega-Linter] Apply linters automatic fixes" | |
| labels: bot | |
| - name: Create PR output | |
| if: steps.changes.outputs.changed == 1 && (env.APPLY_FIXES_EVENT == 'all' || env.APPLY_FIXES_EVENT == github.event_name) && env.APPLY_FIXES_MODE == 'pull_request' | |
| run: | | |
| echo "Pull Request Number - ${{ steps.cpr.outputs.pull-request-number }}" | |
| echo "Pull Request URL - ${{ steps.cpr.outputs.pull-request-url }}" | |
| # Push new commit if applicable | |
| - name: Prepare commit | |
| if: steps.changes.outputs.changed == 1 && (env.APPLY_FIXES_EVENT == 'all' || env.APPLY_FIXES_EVENT == github.event_name) && env.APPLY_FIXES_MODE == 'commit' && github.ref != 'refs/heads/master' | |
| run: sudo chown -Rc $UID .git/ | |
| - name: Commit and push applied linter fixes | |
| if: steps.changes.outputs.changed == 1 && (env.APPLY_FIXES_EVENT == 'all' || env.APPLY_FIXES_EVENT == github.event_name) && env.APPLY_FIXES_MODE == 'commit' && github.ref != 'refs/heads/master' | |
| uses: stefanzweifel/git-auto-commit-action@v4 | |
| with: | |
| branch: ${{ github.event.pull_request.head.ref || github.head_ref || github.ref }} | |
| commit_message: "[Mega-Linter] Apply linters fixes" |