Add html_of_wiki but requires manual build and deployment. - Githubissues

ocsigen / ocsigen.github.io

Ocsigen Web site

https://ocsigen.github.io/

6 stars 8 forks source link

Add html_of_wiki but requires manual build and deployment. #25

Closed leovalais closed 5 years ago

leovalais commented 5 years ago

Depends on

How to use it

make local: creates the website files with links suited for local navigation
make website: creates the files suited for GitHub Pages
make commit: ditto, but git add the files and takes you to the $EDITOR for commiting
make deploy: ditto, but also pushes to master, thus deploying the website