From 6a7d93e70eec43c8c0262ff462117ba2f5580134 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 12 Apr 2024 00:56:23 +0200 Subject: [PATCH] style linter on PRs, add line in Readme --- .github/workflows/push_pr.yml | 9 +++++++++ README.md | 1 + 2 files changed, 10 insertions(+) diff --git a/.github/workflows/push_pr.yml b/.github/workflows/push_pr.yml index 5990d43..02ca1ef 100644 --- a/.github/workflows/push_pr.yml +++ b/.github/workflows/push_pr.yml @@ -2,6 +2,15 @@ on: pull_request: jobs: + style_lint: + name: Lint style + runs-on: ubuntu-latest + steps: + - name: Check for long lines + if: always() + run: | + ! (find BonnAnalysis -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://') + build_project: runs-on: ubuntu-latest name: Build project diff --git a/README.md b/README.md index 2182da1..76bf3c9 100644 --- a/README.md +++ b/README.md @@ -84,5 +84,6 @@ If you feel adventurous and want to build the web version of the blueprint local - Just after you push [this page](https://github.com/fpvandoorn/BonnAnalysis) will have a message on the top prompting you to open a pull request. * If it builds, I'll merge it. + - Feel free to make a pull request with partial work and a lot of sorry's, as long as it builds. Reminder: Some additional details can be found in the instructions of the LeanCourse repository: https://github.com/fpvandoorn/LeanCourse23/blob/master/LeanCourse/Project/README.md \ No newline at end of file