search

leanprover-community / lean4-metaprogramming-book

https://leanprover-community.github.io/lean4-metaprogramming-book/
Apache License 2.0
204 stars 47 forks source link

Resolve duplication issues in README and SUMMARY #126

Closed Seasawher closed 6 months ago

Seasawher commented 6 months ago

see: https://github.com/leanprover-community/lean4-metaprogramming-book/pull/121#issuecomment-1883837074

summary: README is used for pandoc, SUMMARY for mdbook. These two pieces of information are duplicated, which can lead to forgotten changes.

Julian commented 6 months ago

Fixed in #129.

Seasawher commented 6 months ago

it is sure that README does not have duplication. but CONTENTS has still duplication. I think this problem is not fixed yet

Julian commented 6 months ago

Ah, true! Thanks.