Fixed: https://bugzilla.mozilla.org/show_bug.cgi?id=969887#c1. It will take effect with the next re-index, in a few hours.
Good eye! Somehow, nobody caught this on staging or locally, though it seems obvious in retrospect. While I was at it, I stopped the code from jumping to the side when you click a long line number; that was silly, too. Keep the feedback coming, pro and con. We already have many little things on the chopping block: see the high-ID bugs at https://bugzilla.mozilla.org/buglist.cgi?product=Webtools&component=DXR&resolution=---&list_id=9393813. And of course, patches are welcome. :-) Cheers, Erik On Feb 8, 2014, at 6:22 , Tom Schuster <t...@schuster.me> wrote: > The design looks really fresh, I really like the new colors. I am however > wondering about additional spaces that were introduced, they seem to even > break > indentation:http://dxr.mozilla.org/mozilla-central/source/js/src/jsapi.cpp#1426. _______________________________________________ dev-platform mailing list dev-platform@lists.mozilla.org https://lists.mozilla.org/listinfo/dev-platform
