Actually sync the drdoctr.github.io build#241

asmeurer wants to merge 1 commit into

masterdrdoctr/doctr:masterfrom

github.io-pushdrdoctr/doctr:github.io-pushCopy head branch name to clipboard