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] - chore: don't import Lake under Mathlib #13779

Closed
wants to merge 14 commits into from
Closed

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

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
    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
    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
    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
    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
    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
    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
    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
    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. Merge branch 'master' into mrb/revert_13339

    @mattrobball
    mattrobball committed Jun 14, 2024
    Configuration menu
    Copy the full SHA
    58901b2 View commit details
    Browse the repository at this point in the history

  7. Update lakefile.lean

    @mattrobball
    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
    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
    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. Merge remote-tracking branch 'refs/remotes/origin/mrb/revert_13339' i… 

    …nto mrb/revert_13339
    @mattrobball
    mattrobball committed Jun 14, 2024
    Configuration menu
    Copy the full SHA
    bc13d61 View commit details
    Browse the repository at this point in the history

  11. Update lakefile.lean

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