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

get 100.yaml, overview.yaml and undergrad.yaml from mathlib_docs #125

Merged
merged 3 commits into from Sep 2, 2020
Merged

get 100.yaml, overview.yaml and undergrad.yaml from mathlib_docs #125

merged 3 commits into from Sep 2, 2020

Conversation

bryangingechen
Copy link
Collaborator

@bryangingechen bryangingechen commented Sep 1, 2020 •
edited

cf. Zulip thread, leanprover-community/mathlib#4016, and leanprover-community/doc-gen#60.

I also updated .gitignore and README.md and also moved all the urllib.request.urlretrieve lines next to where the downloaded files were used in make_site.py.

PatrickMassot
PatrickMassot reviewed Sep 2, 2020
View reviewed changes
Copy link
Member

@PatrickMassot PatrickMassot left a comment

Choose a reason for hiding this comment

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

Thanks! I don't like all those lonely parentheses, I hope I'm not the author of any of those.

make_site.py Outdated Show resolved Hide resolved
make_site.py Outdated Show resolved Hide resolved
make_site.py Outdated Show resolved Hide resolved
make_site.py Outdated Show resolved Hide resolved
make_site.py Outdated Show resolved Hide resolved
make_site.py Outdated Show resolved Hide resolved
templates/mathlib-overview.html Show resolved Hide resolved
@PatrickMassot PatrickMassot merged commit 41a0d71 into newsite Sep 2, 2020
@PatrickMassot PatrickMassot deleted the yamls_moved_to_mathlib branch September 2, 2020 15:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@PatrickMassot PatrickMassot PatrickMassot left review comments

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@bryangingechen @PatrickMassot