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.

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

feat: detect default target on runLinter #811

Open
wants to merge 15 commits into
base: main
Choose a base branch
from

Commits on May 26, 2024

  1. feat: detect the first default target lean lib on runLinter

    Previously, the default behavior for `runLinter` was to lint
    `Batteries`.
    Now `runLinter` will try to detect the either
    the first lean_exe or first lean_lib
    in Lake's environment which is also a default_target
    austinletson committed May 26, 2024
    Configuration menu
    Copy the full SHA
    a9fd06a View commit details
    Browse the repository at this point in the history

Commits on May 27, 2024

  1. Configuration menu
    Copy the full SHA
    00feb20 View commit details
    Browse the repository at this point in the history

Commits on May 29, 2024

  1. Configuration menu
    Copy the full SHA
    3228792 View commit details
    Browse the repository at this point in the history

Commits on May 30, 2024

  1. Configuration menu
    Copy the full SHA
    3166796 View commit details
    Browse the repository at this point in the history

Commits on Jun 21, 2024

  1. style: add period

    austinletson committed Jun 21, 2024
    Configuration menu
    Copy the full SHA
    7e0847c View commit details
    Browse the repository at this point in the history

Commits on Jul 24, 2024

  1. Configuration menu
    Copy the full SHA
    9106595 View commit details
    Browse the repository at this point in the history

Commits on Nov 2, 2024

  1. Configuration menu
    Copy the full SHA
    1c72942 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    46df64a View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    273182e View commit details
    Browse the repository at this point in the history
  4. Configuration menu
    Copy the full SHA
    c8e3a54 View commit details
    Browse the repository at this point in the history
  5. Configuration menu
    Copy the full SHA
    8f33cf6 View commit details
    Browse the repository at this point in the history
  6. Configuration menu
    Copy the full SHA
    9c4e7ea View commit details
    Browse the repository at this point in the history

Commits on Nov 4, 2024

  1. Configuration menu
    Copy the full SHA
    1510d4c View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    b65cc1e View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    2aaa65a View commit details
    Browse the repository at this point in the history