On 19 May 2014, at 09:10, Jochen Topf <jochen at remote.org> wrote: > You probably just have an old Javascript file cached or so. Try Shift-Reload in > the Browser. That hit the spot. Thanks!