diff --git a/Doc/tools/getpagecounts b/Doc/tools/getpagecounts index 7ede6b89595..e701e941c70 100755 --- a/Doc/tools/getpagecounts +++ b/Doc/tools/getpagecounts @@ -6,18 +6,35 @@ cd `dirname $0`/.. PAPER=${PAPER:-letter} +TOTAL=0 +getpagecount() { + PAGECOUNT=`grep -c '^%%Page:' paper-$PAPER/$1.ps` + echo "$2 $1.ps ($PAGECOUNT pages)" + TOTAL=`expr $TOTAL + $PAGECOUNT` +} cat <