1 files changed, 19 insertions, 0 deletions
diff --git a/util.sh b/util.sh
new file mode 100755
index 0000000..7ad42c8
--- /dev/null
+++ b/util.sh
@@ -0,0 +1,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
+}
+