#! /usr/bin/gawk
# Last edited on 2025-07-04 16:40:59 by stolfi
# Common functions for scripts of Notes/074.
# To be included in other gawk scripts.