Issue 3796 - Added preference to remove developer tools panel

lib/prefs.js

Index: lib/prefs.js
===================================================================
--- a/lib/prefs.js
+++ b/lib/prefs.js
@@ -156,6 +156,13 @@
 defaults.notifications_ignoredcategories = [];
 
 /**
+ * Whether to show the developer tools panel.
+ *
+ * @type {boolean}
+ */
+defaults.show_devtools_panel = true;

[Thomas Greiner, 2016/03/14 16:26:05]

Since there's no mention in the devtools panel on how to disable it, it might be
better to make it opt-in. Personally, I don't have a preference but hiding it in
the options page for people who want to add it seems a bit better than hiding it
in the options page for people who want to get rid of it.

[Sebastian Noack, 2016/03/14 16:39:35]

It's already bad enough that we cannot integrate it into the icon menu. Also
disabling it by default, would make sure that nobody will every find that
feature.

There are no negative side effects of having the panel in the devtools, except
for aesthetic preferences of some users who frequently use the devtools, but
don't need our panel there. So I think having it opt-out is good enough.

[kzar, 2016/03/14 17:52:20]

Sebastian asked me for a third opinion in IRC so here you go:

17:49 <kzar> I think his argument makes sense that it should be
             hidden for "normal" people, but it _already is_ hidden
             for them as they wouldn't use the developer console
             anyway.
17:49 <kzar> So I think it makes sense like it is, it only really
             makes sense to hide the tab if you're a geek and
             somehow really care about how your developer window
             looks

+
+/**
   * @namespace
   * @static
   */