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

[Merged by Bors] - chore: don't import Lake under Mathlib #13779

Closed
wants to merge 14 commits into from

Commits on Jun 12, 2024

  1. Revert "refactor: tweak and move functionality for getting all module…

    …s out of `scripts` (#13339)"
    
    This reverts commit bffb043.
    mattrobball committed Jun 12, 2024
    Configuration menu
    Copy the full SHA
    51d110d View commit details
    Browse the repository at this point in the history
  2. add back

    mattrobball committed Jun 12, 2024
    Configuration menu
    Copy the full SHA
    9d4d9e4 View commit details
    Browse the repository at this point in the history

Commits on Jun 13, 2024

  1. nolints

    mattrobball committed Jun 13, 2024
    Configuration menu
    Copy the full SHA
    87579f6 View commit details
    Browse the repository at this point in the history

Commits on Jun 14, 2024

  1. Revert "nolints"

    This reverts commit 87579f6.
    mattrobball committed Jun 14, 2024
    Configuration menu
    Copy the full SHA
    355f1b8 View commit details
    Browse the repository at this point in the history
  2. add back to Mathlib.lean

    mattrobball committed Jun 14, 2024
    Configuration menu
    Copy the full SHA
    d2f495e View commit details
    Browse the repository at this point in the history
  3. blank file

    mattrobball committed Jun 14, 2024
    Configuration menu
    Copy the full SHA
    18cb303 View commit details
    Browse the repository at this point in the history
  4. remove import

    mattrobball committed Jun 14, 2024
    Configuration menu
    Copy the full SHA
    9ab3ce4 View commit details
    Browse the repository at this point in the history
  5. fix

    mattrobball committed Jun 14, 2024
    Configuration menu
    Copy the full SHA
    16c93ae View commit details
    Browse the repository at this point in the history
  6. Configuration menu
    Copy the full SHA
    58901b2 View commit details
    Browse the repository at this point in the history
  7. Update lakefile.lean

    mattrobball authored Jun 14, 2024
    Configuration menu
    Copy the full SHA
    a36477a View commit details
    Browse the repository at this point in the history
  8. Update lakefile.lean

    mattrobball authored Jun 14, 2024
    Configuration menu
    Copy the full SHA
    4d271bd View commit details
    Browse the repository at this point in the history
  9. cleanup

    mattrobball committed Jun 14, 2024
    Configuration menu
    Copy the full SHA
    8738b00 View commit details
    Browse the repository at this point in the history
  10. Configuration menu
    Copy the full SHA
    bc13d61 View commit details
    Browse the repository at this point in the history
  11. Update lakefile.lean

    mattrobball authored Jun 14, 2024
    Configuration menu
    Copy the full SHA
    3d9182a View commit details
    Browse the repository at this point in the history