+ * Log an Event Log entry. Used in SSH packet logging mode; this is
+ * also as convenient a place as any to put the output of Event Log
+ * entries to stderr when a command-line tool is in verbose mode.
+ * (In particular, this is a better place to put it than in the
+ * front ends, because it only has to be done once for all
+ * platforms. Platforms which don't have a meaningful stderr can
+ * just avoid defining FLAG_STDERR.