1.1 --- a/tools/mappings.sh Tue Jul 16 23:52:15 2013 +0200
1.2 +++ b/tools/mappings.sh Tue Jul 16 23:54:52 2013 +0200
1.3 @@ -3,10 +3,10 @@
1.4 PROGNAME=`basename $0`
1.5 THISDIR=`dirname $0`
1.6
1.7 -MAPPINGS=$*
1.8 +SPACES=$*
1.9
1.10 -if [ ! "$MAPPINGS" ]; then
1.11 - echo "$PROGNAME <mapping file>..."
1.12 +if [ ! "$SPACES" ]; then
1.13 + echo "$PROGNAME <space directory>..."
1.14 exit 1
1.15 fi
1.16
1.17 @@ -17,7 +17,7 @@
1.18
1.19 # Combine the space mappings into a common mapping from page identifiers to
1.20 # page names.
1.21 -sort -n -u $MAPPINGS > "$ID_MAPPING"
1.22 +sort -n -u `find $SPACES -name MAPPING` > "$ID_MAPPING"
1.23
1.24 # Produce a common mapping from tiny URL identifiers to page names.
1.25 cut -f 1 "$ID_MAPPING" | uniq | "$THISDIR/tiny.py" - > "$TINY_ID_MAPPING"