#! /bin/bash -eu
# Last edited on 2026-06-04 15:25:41 by stolfi