#! /bin/bash -eu
# Last edited on 2026-02-16 18:00:54 by stolfi

# Trick to make "-f" unnecessary on the "#!" line of gawk scripts
# and alloy more than one option to be passed to it.

pwd 1>&2
echo "options = --lint=fatal -f $@" 1>&2
/usr/bin/gawk --lint=fatal -f "$@"