<div dir="ltr">That must be a bug.<div><div><br></div><div>Karl</div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, May 4, 2015 at 11:27 PM, Chris Muller <span dir="ltr"><<a href="mailto:asqueaker@gmail.com" target="_blank">asqueaker@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Mon, May 4, 2015 at 4:18 PM, Chris Muller <<a href="mailto:asqueaker@gmail.com">asqueaker@gmail.com</a>> wrote:<br>
> One thing I don't like about the scattered preferences is how the<br>
> preference API is no longer supported. I have a script which sets up<br>
> my preferred preferences, I tried to write:<br>
><br>
> Preferences disable: #showMessageIcons<br>
><br>
> just like I can for "normal" preferences, however, the above doesn't<br>
> work and doesn't report an error...<br>
<br>
</span>In fact, it can even cause a duplicate preference to be added (see picture).<br>
<br><br>
<br></blockquote></div><br></div>