I do see mentions of gh-pages in the build_docs.sh script - is devstack.org redirect to GitHub? -- Sean M. Collins