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

doc: add tips about lake usage #510

Open
wants to merge 10 commits into
base: lean4
Choose a base branch
from
Open

doc: add tips about lake usage #510

wants to merge 10 commits into from

Commits on Aug 2, 2024

  1. doc: add tips about lake usage

    @joneugster
    joneugster committed Aug 2, 2024
    Configuration menu
    Copy the full SHA
    d91448a View commit details
    Browse the repository at this point in the history

  2. update lake doc link

    @joneugster
    joneugster committed Aug 2, 2024
    Configuration menu
    Copy the full SHA
    4eee323 View commit details
    Browse the repository at this point in the history

  3. update text

    @joneugster
    joneugster committed Aug 2, 2024
    Configuration menu
    Copy the full SHA
    5086492 View commit details
    Browse the repository at this point in the history

  4. add comment

    @joneugster
    joneugster committed Aug 2, 2024
    Configuration menu
    Copy the full SHA
    c22f5d4 View commit details
    Browse the repository at this point in the history

  5. use word dependency instead of package

    @joneugster
    joneugster committed Aug 2, 2024
    Configuration menu
    Copy the full SHA
    04f87fe View commit details
    Browse the repository at this point in the history

  6. wording

    @joneugster
    joneugster committed Aug 2, 2024
    Configuration menu
    Copy the full SHA
    0af416f View commit details
    Browse the repository at this point in the history

Commits on Sep 5, 2024

  1. Apply suggestions from code review 

    Co-authored-by: grunweg <[email protected]>
    @joneugster @grunweg
    joneugster and grunweg authored Sep 5, 2024
    Configuration menu
    Copy the full SHA
    b658096 View commit details
    Browse the repository at this point in the history

  2. address suggestions

    @joneugster
    joneugster committed Sep 5, 2024
    Configuration menu
    Copy the full SHA
    30140c5 View commit details
    Browse the repository at this point in the history

  3. fix

    @joneugster
    joneugster committed Sep 5, 2024
    Configuration menu
    Copy the full SHA
    b402afc View commit details
    Browse the repository at this point in the history

  4. whitespace

    @joneugster
    joneugster committed Sep 5, 2024
    Configuration menu
    Copy the full SHA
    605b411 View commit details
    Browse the repository at this point in the history