chmod options reference

diff --git a/push-to-web.sh b/push-to-web.sh
index e888f02..422f0fd 100755 (executable)
--- a/push-to-web.sh
+++ b/push-to-web.sh
@@ -14,6 +14,7 @@ site=$1
 
 # Generate documentation.
 ./generate-documentation.py > docs/options.html
+chmod a+r docs/options.html
 if [ -s docs/options.html ] ; then
   ./generate-jsdoc.sh