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.

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

fix issue on mdbook config #137

Merged
merged 6 commits into from
Apr 15, 2024

Conversation

Seasawher
Copy link
Contributor

The current directory should not be specified as the src directory. This causes a problem where the .git directory is copied into the book directory.

The current directory should not be specified as the src directory. This causes a problem where the `.git` directory is copied into the `book` directory.
@Seasawher

This comment was marked as resolved.

@Seasawher Seasawher force-pushed the fix-mdbook-setting branch 2 times, most recently from 90e45f5 to 2b21cd5 Compare April 8, 2024 18:16
@Seasawher Seasawher force-pushed the fix-mdbook-setting branch from 2b21cd5 to 28a93bf Compare April 8, 2024 18:25
@Seasawher Seasawher marked this pull request as draft April 11, 2024 10:45
@Seasawher

This comment was marked as outdated.

@Seasawher
Copy link
Contributor Author

this PR also fix issue #121 (comment)

@Seasawher Seasawher marked this pull request as ready for review April 11, 2024 11:57
@Julian
Copy link
Collaborator

Julian commented Apr 15, 2024

Looks good to me I think. Thanks again!

@Julian Julian merged commit 7119967 into leanprover-community:master Apr 15, 2024
4 checks passed
@Seasawher Seasawher deleted the fix-mdbook-setting branch April 15, 2024 18:45
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants