You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
|
#!/bin/bash
|
|
#
|
|
# Utility functions, used by demo.sh and regtest.sh.
|
|
|
|
banner() {
|
|
echo
|
|
echo "----- $@"
|
|
echo
|
|
}
|
|
|
|
log() {
|
|
echo 1>&2 "$@"
|
|
}
|
|
|
|
die() {
|
|
log "$0: $@"
|
|
exit 1
|
|
}
|
|
|
