doc: add a .nojekyll to gh pages and ignore submodules

publish-gh-pages

@@ -9,10 +9,16 @@ git checkout master -- \
   '*.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 --message "$(git log -n1 --pretty='%H' master)"
-git push
+git commit --allow-empty --message "$(git log -n1 --pretty='%H' master)"
+git push -f
 git checkout -