using mdgen instead of lean2md #123
Conversation
Seasawher
changed the title
|
By the way, since the contents of the |
There was a problem hiding this comment.
Should the contents of the lean directory be respected or the md directory?
The diff here looks correct (i.e. the changes look like an improvement) -- probably what happened was that lean2md wasn't run on the .lean files -- you generated the PR from those (the .lean files), correct?
| @@ -8,6 +8,9 @@ lean_lib «lean4-metaprogramming-book» where | |||
| roots := #[`cover, `extra, `main, `solutions] | |||
| globs := #[Glob.one `cover, Glob.submodules `extra, Glob.submodules `main, Glob.submodules `solutions] | |||
|
|
|||
| require mdgen from git | |||
There was a problem hiding this comment.
Can you publish a release (and put that here) so we don't run into silent breakage if something changes?
| @@ -17,23 +20,3 @@ def runCmd (cmd : String) (args : Array String) : ScriptM Bool := do | |||
| if hasError then | |||
| IO.eprint out.stderr | |||
| return hasError | |||
|
|
|||
| script build do | |||
There was a problem hiding this comment.
Perhaps it's worth leaving lake run build in place and simply updating it -- that makes it slightly easier for someone to build the md files if needed, without needing to look up mdgen's CLI syntax.
|
Thanks! This looks pretty good to me! I didn't try running mdgen yet, but I'll do that. As for
That sounds good to me as well, will have a look at that PR. |
|
@Julian I have made corrections to the points you pointed out. |
|
This looks good I think! Let's merge and see how it goes. Thanks! |
resolve #122
@arthurpaulino Replacing lean2md with mdgen does not seem to break the markdown file. However, the contents of the files in the lean directory are different from the contents of the files in the md directory, resulting in a large number of diffs. What should I do?
Should the contents of the
leandirectory be respected or themddirectory?