#!/bin/bash # A very simple script. But sufficient, hopefully, for our current purposes. cat <