/* This file exists because "util.h" is such a generic name that it is
likely to clash with other such files. */
#include "util.h"