From 99cef0df6a6de75cafa9950d00024689eaeeadb2 Mon Sep 17 00:00:00 2001
From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Wed, 20 Mar 2019 23:49:40 +0000
Subject: [PATCH] rename text files to end in .txt in www

So that they get the right Content-Type
---
 Makefile | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/Makefile b/Makefile
index 9bc7095..eec3024 100644
--- 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
-- 
2.30.2