fix issue on mdbook config

leanprover-community / lean4-metaprogramming-book

https://leanprover-community.github.io/lean4-metaprogramming-book/

Apache License 2.0

204 stars 47 forks source link

fix issue on mdbook config #137

Closed Seasawher closed 3 months ago

Seasawher commented 3 months ago

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 commented 3 months ago

@Julian I don't know why the build of the PDF fails. Could you help me, please?

Seasawher commented 3 months ago

memo: expected out put of $(grep ...) command:

md/main/01_intro.md
md/main/02_overview.md

correct command:

grep -o '\(\/.*\.md\)' md/SUMMARY.md | sed 's/^/md/'

Seasawher commented 3 months ago

this PR also fix issue https://github.com/leanprover-community/lean4-metaprogramming-book/pull/121#discussion_r1447642044

Julian commented 3 months ago

Looks good to me I think. Thanks again!