util.sh


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

#!/bin/bash
#
# Utility functions, used by demo.sh and regtest.sh.

banner() {
  echo
  echo "----- $@"
  echo
}

log() {
  echo 1>&2 "$@"
}

die() {
  log "$0: $@"
  exit 1
}