#! /usr/bin/gawk -f
# Last edited on 2026-09-09 09:27:07 by stolfi