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

[Merged by Bors] - feat: rewrite set_option style linter in lean #12928

Closed
wants to merge 7 commits into from
Closed

[Merged by Bors] - feat: rewrite set_option style linter in lean #12928

wants to merge 7 commits into from

Commits on May 24, 2024

  1. feat: rewrite set_option style linter in lean 

    Unlike the Python version, this script also supports set_option tactics
and terms.
    @grunweg
    grunweg committed May 24, 2024
    Configuration menu
    Copy the full SHA
    082a07c View commit details
    Browse the repository at this point in the history

  2. Fix setOption linter in tests: mostly disable it; in one instance, on… 

    …e option could be simply removed.
    @grunweg
    grunweg committed May 24, 2024
    Configuration menu
    Copy the full SHA
    da89b47 View commit details
    Browse the repository at this point in the history

  3. Add to file of all linters.

    @grunweg
    grunweg committed May 24, 2024
    Configuration menu
    Copy the full SHA
    5017c0c View commit details
    Browse the repository at this point in the history

Commits on May 26, 2024

  1. Fix namespace of the linter option.

    @grunweg
    grunweg committed May 26, 2024
    Configuration menu
    Copy the full SHA
    2f7dea6 View commit details
    Browse the repository at this point in the history

Commits on May 29, 2024

  1. Use Syntax.find instead

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

  2. Syntax tweaks.

    @grunweg
    grunweg committed May 29, 2024
    Configuration menu
    Copy the full SHA
    6ac63fb View commit details
    Browse the repository at this point in the history

Commits on May 31, 2024

  1. Merge branch 'master' into MR-rewrite-setOption

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