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(README): fix docs for building documentation locally #14114

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - chore(README): fix docs for building documentation locally #14114

wants to merge 4 commits into from

Conversation

kim-em
Copy link
Contributor

@kim-em kim-em commented Jun 25, 2024

Open in Gitpod

@kim-em kim-em added documentation Improvements or additions to documentation awaiting-review labels Jun 25, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 25, 2024
jcommelin
jcommelin reviewed Jun 26, 2024
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors d+

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jun 26, 2024

✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

kim-em and others added 2 commits July 1, 2024 16:40
@kim-em @jcommelin
Update README.md
a1eefa3 
Co-authored-by: Johan Commelin <[email protected]>
@kim-em
merge
61c32d0
@kim-em kim-em removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 1, 2024
@github-actions GitHub Actions
Copy link

github-actions bot commented Jul 1, 2024

PR summary 954b5ecb61

Import changes

No significant changes to the import graph

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows 
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

@jcommelin
Copy link
Member

Thanks 🎉

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jul 5, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jul 5, 2024
@kim-em
chore(README): fix docs for building documentation locally (#14114)
215c891
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jul 5, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(README): fix docs for building documentation locally [Merged by Bors] - chore(README): fix docs for building documentation locally Jul 5, 2024
@mathlib-bors mathlib-bors bot closed this Jul 5, 2024
@mathlib-bors mathlib-bors bot deleted the README_docs branch July 5, 2024 09:32
@adomani adomani mentioned this pull request Aug 1, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin left review comments

Assignees
No one assigned
Labels
documentation Improvements or additions to documentation ready-to-merge This PR has been sent to bors.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@kim-em @jcommelin @leanprover-community-mathlib4-bot