index 7c08e99c4854bdeb98c0342a79f05c9507605847..e35d7811acc60415e38e58866b5488938d0372a4 100755 (executable)
for mode in no-notes notes
do
echo $mode
- /usr/bin/time sh ../time_notes $mode $1
+ /usr/bin/time "$SHELL_PATH" ../time_notes $mode $1
done
}