1#!/bin/bash 2# 3# Utility functions, used by demo.sh and regtest.sh. 4 5banner() { 6 echo 7 echo "----- $@" 8 echo 9} 10 11log() { 12 echo 1>&2 "$@" 13} 14 15die() { 16 log "$0: $@" 17 exit 1 18} 19 20