| keysize=${line%%;*}; |
keysize=${line%%;*}; |
| keysize=${keysize#* }; |
keysize=${keysize#* }; |
| |
|
| if ! expr match "$keysizes" ".*$keysize.*" &> /dev/null; then |
if ! expr "$keysizes" : ".*$keysize.*" &> /dev/null; then |
| echo " ${line//href=\'/href=\'$dir/}"; |
echo " ${line//href=\'/href=\'$dir/}"; |
| keysizes="$keysizes $keysize"; |
keysizes="$keysizes $keysize"; |
| fi |
fi |
| make_footer >> index.html; |
make_footer >> index.html; |
| ) |
) |
| done | sort -n | while read line; do |
done | sort -n | while read line; do |
| if expr match "$line" ".*/benchmarks/" &> /dev/null; then |
if expr "$line" : ".*/benchmarks/" &> /dev/null; then |
| line=${line/"<tr>"/"<tr class='benchmark'>"}; |
line=${line/"<tr>"/"<tr class='benchmark'>"}; |
| fi |
fi |
| |
|
