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