subdirectories of src about format_lean

[PatrickMassot]

I should remove the format_lean command, it's mostly for testing purposes. The real thing is format_project. There I can't reproduce your problem. Could you post a full archive of a minimal example?

[kbuzzard]

Jason's repo https://github.com/JasonKYi/M4000x_LEAN_formalisation used to work but now format_project is giving us html files which aren't clickable. Maybe there's some syntax error somewhere but we have no idea how to debug.

[PatrickMassot]

I'm sorry I can't reproduce that problem. I just cloned the repository, leanpkg configure, update-mathlib and format_project and everything works except that the broken link tag at https://github.com/JasonKYi/M4000x_LEAN_formalisation/blob/master/src/M40001/M40001_C2.lean#L27 (a <a> should be </a>) messes up the rendering in Firefox (everything gets underlined after that point). By the way, you can use markdown links.

[kbuzzard]

I clone the repo, leanpkg configure, update-mathlib, format_project, change directory into html, start a web server in this directory, and then navigate to M40001 and I have a bunch of unclickable stuff in the html files. How can I debug this? I'm on Ubuntu 18.04.

[PatrickMassot]

Fixed in 1122e2b