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

/^ *([#]|$)/ { next; }

/^<f10[3456789][rv]/ { print; next; }
/^<f11[012345][rv]/ { print; next; }

/^<f116r[.]([0-9]|[12][0-9]|30)[,;>]/ { print; next; }

//{ next; }