# a handy little method that can be used for date strings. it was getting
# really tiresome how many different ways the script did the date formatting.
function date_stringer() {
- date +"%Y_%m_%d_%H%M_%S" | tr -d '/\n/'
+ local sep="$1"; shift
+ if [ -z "$sep" ]; then sep='_'; fi
+ date +"%Y$sep%m$sep%d$sep%H%M$sep%S" | tr -d '/\n/'
}
# makes a directory of the name specified and then tries to change the
| grep -i "$i" \
| sed -n -e "$appropriate_pattern")
if [ ${#PIDS_SOUGHT[*]} -ne 0 ]; then
- # we want to bail as soon as we get matches, because on the same
- # platform, the same set of patterns should work to find all
- # occurrences of the genesis java.
+ # we want to bail as soon as we get matches, because on the same
+ # platform, the same set of patterns should work to find all
+ # occurrences of the genesis java.
break;
fi
done
| grep -i "$i" \
| sed -n -e "$appropriate_pattern")
if [ ${#PIDS_SOUGHT[*]} -ne 0 ]; then
- # we want to bail as soon as we get matches, because on the same
- # platform, the same set of patterns should work to find all
- # occurrences of the genesis java.
+ # we want to bail as soon as we get matches, because on the same
+ # platform, the same set of patterns should work to find all
+ # occurrences of the genesis java.
break;
fi
done