/* placeholder to work around brain-dead inconsistent JS implementation
 in a certain Web browser that shall remain nameless */