# HG changeset patch
# User Paul Boddie <paul@boddie.org.uk>
# Date 1374011692 -7200
# Node ID e75a20e9f7c5face0b48a68f3ceffd8f1a2cf8de
# Parent  779f66c84247e277098c0abcb61ac2492dc30b82
Made the script use space directories instead of mapping files directly.

diff -r 779f66c84247 -r e75a20e9f7c5 tools/mappings.sh
--- a/tools/mappings.sh	Tue Jul 16 23:52:15 2013 +0200
+++ b/tools/mappings.sh	Tue Jul 16 23:54:52 2013 +0200
@@ -3,10 +3,10 @@
 PROGNAME=`basename $0`
 THISDIR=`dirname $0`
 
-MAPPINGS=$*
+SPACES=$*
 
-if [ ! "$MAPPINGS" ]; then
-	echo "$PROGNAME <mapping file>..."
+if [ ! "$SPACES" ]; then
+	echo "$PROGNAME <space directory>..."
 	exit 1
 fi
 
@@ -17,7 +17,7 @@
 
 # Combine the space mappings into a common mapping from page identifiers to
 # page names.
-sort -n -u $MAPPINGS > "$ID_MAPPING"
+sort -n -u `find $SPACES -name MAPPING` > "$ID_MAPPING"
 
 # Produce a common mapping from tiny URL identifiers to page names.
 cut -f 1 "$ID_MAPPING" | uniq | "$THISDIR/tiny.py" - > "$TINY_ID_MAPPING"