# HG changeset patch
# User Jim Hague <jim.hague@acm.org>
# Date 1377089512 -3600
# Node ID 5628fcd6c692e23e87ad6641c017b3e986881f07
# Parent  7240535f9fa7f8a372961ba733958b87c11e3fa3
Don't mark SSI files executable.

We now archive to publish, and archiving loses the executable bit, so I've
had to enable SSI for all .html anyway.

diff -r 7240535f9fa7 -r 5628fcd6c692 makeWeb.sh
--- a/makeWeb.sh	Wed Aug 21 11:03:36 2013 +0100
+++ b/makeWeb.sh	Wed Aug 21 13:51:52 2013 +0100
@@ -49,9 +49,6 @@
 sed -e "s/@BUILD@/$buildno/" -e "s/@SUBTITLE@/$subtitle/" \
     -e "s/@TITLE@/$title/" -e "s/@BOOK@/$booke/" dottes.html > $webdir/$output
 
-# Mark output as executable so it is scanned for server-side includes.
-chmod +x $webdir/$output
-
 for item in intro
 do
     rm -f $webdir/$item.html