[skip changelog] document the docs generation workflow#738

Merged

rsora merged 3 commits intomasterfrom

massi/document-docs

Jun 10, 2020

Commits on Jun 3, 2020

[skip changelog] document the docs generation workflow

Massimiliano Pippi
authored and
masci
committed
clarify how humans should not push to gh-pages

Massimiliano Pippi
authored and
masci
committed

Commits on Jun 4, 2020

Apply suggestions from code review

Massimiliano Pippi
and
per1234
authored