math-comp / mcb

Mathematical Components (the Book)
Other
140 stars 25 forks source link

Fix .v files + jscoq #121

Closed gares closed 3 years ago

gares commented 3 years ago

Hello @andreykl I took the liberty to push here your changes and add a commit fixing the compilation. Many thanks for your work!

I'm not very knowledgeable of npm & co... would it be possible to deploy website on the book website?

andreykl commented 3 years ago

Hello Enrico,

thank you.

As for placing files to book website I think I need create task in Makefile which creates folder with static version of site which can be placed to website. I think I will do it in a couple days if it is okay.

As for fix compilation. A bit strange to me, on my PC this Makefile works. It is possible this is about different shells, I do not know the make too good.

I commited several changes include file naming changes that can break building process I think.. Could you let me know what shell do you use?