From b7d36956d0b31d38788b9508e2de9f1047395c1f Mon Sep 17 00:00:00 2001
From: Dan Vanderkam <danvk@google.com>
Date: Mon, 23 Apr 2012 12:24:12 -0400
Subject: [PATCH] chmod options reference

---
 push-to-web.sh | 1 +
 1 file changed, 1 insertion(+)

diff --git a/push-to-web.sh b/push-to-web.sh
index e888f02..422f0fd 100755
--- 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
 
-- 
2.7.4