diff --git a/local/bin/profile_bash.sh b/local/bin/profile_bash.sh
old mode 100755
new mode 100644
index df46157..39eac07
--- a/local/bin/profile_bash.sh
+++ b/local/bin/profile_bash.sh
@@ -1,11 +1,15 @@
 #!/usr/bin/env bash
 #
-# Assumes file descriptor 3 is not messed with in the profiled script.
+# Writes profiling info (resp. accumulated info) to $$.timings (resp.
+# $$.acc_timings) in working directory. The concrete filenames of both files
+# are written to stderr.
+#
+# This script assumes file descriptor 3 is not messed with in the profiled
+# script, nor with the xtrace option of bash.
 
-pid=$$
-exec 3>&2 2> >(tee /tmp/bash_profile-${pid}.log | \
+exec 3>&2 2> >(tee /tmp/bash-profile-$$.log | \
                sed -u 's/^.*$/now/' | \
-               date -f - +%s.%N >/tmp/bash_profile-${pid}.tim)
+               date -f - +%s.%N >/tmp/bash-profile-$$.tim)
 set -x
 
 . "$@"
@@ -18,29 +22,28 @@ paste <(
         crt=000000000$((${tim//.}-10#0$last))
         printf "%12.9f\n" ${crt:0:${#crt}-9}.${crt:${#crt}-9}
         last=${tim//.}
-    done < /tmp/bash_profile-${pid}.tim
-) /tmp/bash_profile-${pid}.log > ${pid}.timings
-
-accumulator='
-{
-    sum[$2] += $1
-    count[$2] += 1
-}
-END {
-    printf("command\ttotal\ttimes\taverage\n")
-    for (key in sum) {
-        printf("%s\t%f\t%d\t%f\n", key, sum[key], count[key], sum[key] / count[key])
-    }
-}
-'
+    done < /tmp/bash-profile-$$.tim
+) /tmp/bash-profile-$$.log > $$.timings
 
 paste \
-    <(cut -f1 ${pid}.timings) \
-    <(cat /tmp/bash_profile-${pid}.log \
-        | sed '/\] *=/c [[assignement]]' \
-        | sed -n 's/++* \([^ ]*\).*/\1/p' \
-        | sed '/=/c [[assignment]]') \
-    | > ${pid}.acc awk "$accumulator"
+    <(cut -f1 $$.timings) \
+    <(cat /tmp/bash-profile-$$.log | \
+        sed 's/^+\+ //' | \
+        sed 's/^\(local\s\|declare\|\S\+=\).*/[[assignment]]/') | \
+    tail -n +2 | \
+    awk '{
+        cumtime[$2] += $1
+        count[$2] += 1
+    }
+    END {
+        printf("cumtime\tcalls\tavg.time\tcommand\n")
+        for (key in cumtime) {
+            printf("%f\t%d\t%f\t%s\n", cumtime[key], count[key],
+                   cumtime[key] / count[key], key)
+        }
+    }' | \
+    sort -k1gr >$$.acc_timings
 
-rm /tmp/bash_profile-${pid}.{tim,log}
-echo ${pid}.timings
+rm /tmp/bash-profile-$$.{tim,log}
+
+echo $$.timings $$.acc_timings >&2