rename text files to end in .txt in www

So that they get the right Content-Type

diff --git a/Makefile b/Makefile
index 9bc7095aed268def55cc7437e15b615e3c15c27c..eec3024c755afc6a602fe58f79e1630c5010ba97 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -35,6 +35,7 @@
 # only nontrivial game description files I know of are indeed such
 # derivatives.
 
+SHELL=/bin/bash
 
 i=mv -f $@.tmp $@
 o= >$@.tmp && $i
@@ -97,6 +98,7 @@ all:          all-ps all-pdf all-preview
 PSS=$(addsuffix .ps,  $(BOARDFILES))
 PDFS=$(addsuffix .pdf, $(BOARDFILES))
 PREVIEWS=maxprintable-a3-preview.png
+TEXTFILES=README map.plag
 
 all-ps:        $(PSS)
 all-pdf:       $(PDFS)
@@ -112,9 +114,11 @@ map.plag: generate-plag input-graph Parse.pm
 
 www=ianmdlvl@chiark:public-html/pandemic-rising-tide
 
-html: $(PDFS) $(PREVIEWS) README map.plag
+html: $(PDFS) $(PREVIEWS) $(TEXTFILES)
        rm -rf $@ $@.tmp; mkdir $@.tmp
-       cp $^ $@.tmp/ && $i
+       cp $^ $@.tmp/
+       set -e; for f in $(TEXTFILES); do mv $@.tmp/$$f{,.txt}; done
+       $i
 
 to-www: html
        git-push