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

Add a CI script to automate "this month in mathlib" #40

Open
wants to merge 11 commits into
base: master
Choose a base branch
from
Open

Add a CI script to automate "this month in mathlib" #40

wants to merge 11 commits into from

Commits on Jun 8, 2022

  1. Add a CI script to automate "this month in mathlib"

    @eric-wieser
    eric-wieser authored Jun 8, 2022
    Configuration menu
    Copy the full SHA
    082a85b View commit details
    Browse the repository at this point in the history

  2. Update make-monthly-pr.yml

    @eric-wieser
    eric-wieser authored Jun 8, 2022
    Configuration menu
    Copy the full SHA
    b887493 View commit details
    Browse the repository at this point in the history

  3. Update make-monthly-pr.yml

    @eric-wieser
    eric-wieser authored Jun 8, 2022
    Configuration menu
    Copy the full SHA
    d7e5dca View commit details
    Browse the repository at this point in the history

  4. Update make-monthly-pr.yml

    @eric-wieser
    eric-wieser authored Jun 8, 2022
    Configuration menu
    Copy the full SHA
    aa27613 View commit details
    Browse the repository at this point in the history

  5. Update make-monthly-pr.yml

    @eric-wieser
    eric-wieser authored Jun 8, 2022
    Configuration menu
    Copy the full SHA
    201c27d View commit details
    Browse the repository at this point in the history

  6. Update make-monthly-pr.yml

    @eric-wieser
    eric-wieser authored Jun 8, 2022
    Configuration menu
    Copy the full SHA
    43710bc View commit details
    Browse the repository at this point in the history

  7. Tidy

    @eric-wieser
    eric-wieser authored Jun 8, 2022
    Configuration menu
    Copy the full SHA
    b17667e View commit details
    Browse the repository at this point in the history

  8. Update make-monthly-pr.yml

    @eric-wieser
    eric-wieser authored Jun 8, 2022
    Configuration menu
    Copy the full SHA
    0c1077c View commit details
    Browse the repository at this point in the history

  9. Update make-monthly-pr.yml

    @eric-wieser
    eric-wieser authored Jun 8, 2022
    Configuration menu
    Copy the full SHA
    17cc19d View commit details
    Browse the repository at this point in the history

  10. Update make-monthly-pr.yml

    @eric-wieser
    eric-wieser authored Jun 8, 2022
    Configuration menu
    Copy the full SHA
    ae7ce34 View commit details
    Browse the repository at this point in the history

  11. Finalize

    @eric-wieser
    eric-wieser authored Jun 8, 2022
    Configuration menu
    Copy the full SHA
    b20c6f5 View commit details
    Browse the repository at this point in the history