fix(bors.toml, build.yml): check for new linter, rename linter to "Li…

…nt style" (#4539) Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
leanprover-community · Oct 8, 2020 · a912455 · a912455
1 parent 73f119e
commit a912455
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -13,7 +13,7 @@ on:
 
 jobs:
   style_lint:
-    name: Check for copyright header, module doc and long lines
+    name: Lint style
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v2

diff --git a/bors.toml b/bors.toml
@@ -1,4 +1,4 @@
-status = ["Build mathlib", "Lint mathlib", "Run tests"]
+status = ["Build mathlib", "Lint mathlib", "Run tests", "Lint style"]
 use_squash_merge = true
 timeout_sec = 21600
 block_labels = ["not-ready-to-merge", "WIP", "blocked-by-other-PR"]