The markdown files are generated automatically via lean2md. Thus, if you're going to write or fix content for the book, please do so in the original Lean files inside the lean directory.
I.e. "change the Lean files then compile, not the markdown files".
This can lead to forgetfulness, see e.g. #111 or #112 or earlier examples.
We likely should at very least add CI which fails a PR if markdown files are changed but not Lean files.
Right now the README tells contributors:
I.e. "change the Lean files then compile, not the markdown files".
This can lead to forgetfulness, see e.g. #111 or #112 or earlier examples.
We likely should at very least add CI which fails a PR if markdown files are changed but not Lean files.