{# Extra javascript that enables copy-to-clipboard for a given element #}