search

coq / coq.github.io

Source files of the coq.inria.fr website
https://coq.inria.fr/
Other
15 stars 37 forks source link

Updated version of nahas tutorial. #90

Closed mdnahas closed 5 years ago

mdnahas commented 5 years ago

I edited the HTML produced by coqdoc to match the header/footer of existing file. Modified the HTML produced by coqdoc to make links work.

I was unable to test this branch locally. I ran "make" and "make run".
Browser correctly loaded homepage at 127.0.0.1:8000 But, when I clicked on "documentation", I got 404 file-not-found error. Same 404 error happens if I try to directly navigate to 127.0.0.1:8000/tutorial-nahas.

I opened dest/tutorial-nahas.html directly in a browser. It rendered, with header and footer. It did not have traditional coqdoc colors, like current version on the website. (This may be because it could not find the CSS file.)

Zimmi48 commented 5 years ago

There is indeed a problem with the current setup: you have to manually add .html to URLs when testing locally. Hopefully, this problem will be fixed when we move away from yamlpp.