Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: rewrite update-style-exceptions.sh as a Lean executable #13245

Closed
wants to merge 5 commits into from
Closed

feat: rewrite update-style-exceptions.sh as a Lean executable #13245

wants to merge 5 commits into from

Commits on May 31, 2024

  1. chore: refactor and move functionality for getting all modules out of… 

    … scripts/

It is needed in other scripts: the easiest way to depend on this is to move this to mathlib. Better places are welcome!
    @grunweg
    grunweg committed May 31, 2024
    Configuration menu
    Copy the full SHA
    629199e View commit details
    Browse the repository at this point in the history

  2. feat: rewrite update_style_exceptions as a Lean executable 

    I'm passing all files as command line arguments: this is not how you're
supposed to do it, but as a stop-gap measure, this is fine.
    @grunweg
    grunweg committed May 31, 2024
    Configuration menu
    Copy the full SHA
    9c6183f View commit details
    Browse the repository at this point in the history

  3. Change the update-nolints workflow accordingly.

    @grunweg
    grunweg committed May 31, 2024
    Configuration menu
    Copy the full SHA
    00109e5 View commit details
    Browse the repository at this point in the history

Commits on Jun 1, 2024

  1. Merge branch 'master' into MR-rewrite-update-style-exceptions

    @grunweg
    grunweg committed Jun 1, 2024
    Configuration menu
    Copy the full SHA
    a23f34f View commit details
    Browse the repository at this point in the history

  2. Small touch-ups; match the naming convention.

    @grunweg
    grunweg committed Jun 1, 2024
    Configuration menu
    Copy the full SHA
    b3faf17 View commit details
    Browse the repository at this point in the history