When writing the previous post, WordPress was seriously trying to prevent me from publishing a link with ‘javascript’ as its protocol (<a href=”javascript:the actual JavaScript was here“>…</a>). As publishing that link was, kinda, the point of the post, I had to make it work.
WordPress Codex’s Using Javascript told me to try a plugin called Text Control, so I installed it, and with No Formatting and No Character Encoding selected, the JavaScript link came to life.