diff options
| -rwxr-xr-x | doc/make-site.sh | 15 | 
1 files changed, 0 insertions, 15 deletions
| diff --git a/doc/make-site.sh b/doc/make-site.sh deleted file mode 100755 index 63a3503..0000000 --- a/doc/make-site.sh +++ /dev/null @@ -1,15 +0,0 @@ -#!/bin/sh - -out=html - -rm ./${out}/*.html - -texi2html --output=${out} \ -    --split=chapter \ -    --noheader \ -    --nonumber-section \ -    --init-file=./site.conf \ -    --top-file=index.html \ -    geiser.texi - -cp geiser.css ${out} | 
