publish-gh-pages

#!/usr/bin/env bash
# https://cirosantilli.com/linux-kernel-module-cheat#github-pages
set -eu
git push
./build-doc --github-pages
git checkout gh-pages
git checkout master -- \
  .gitignore \
  '*.png' \
  _config.yml \
;
touch .nojekyll
# submodules are not deleted on checkout.
# We should not publish like this, we should make a separate tree,
# otherwise files appear and disapear as you publish, which is bad
# for editors. But lazy.
echo 'submodules' >> .gitignore
cp out/README.html index.html
cp out/doc/* .
mv README.html index-split.html
git add .
git commit --allow-empty --message "$(git log -n1 --pretty='%H' master)"
git push -f
git checkout -