index 361a10aeb17108049bf0e47b71153800727edd87..8ab333dbd949fe781b5c13b3deab665544763a88 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
}