Remove newly-added prefs.php cruft

diff --git a/imp/config/prefs.php.dist b/imp/config/prefs.php.dist
index 034ba87..9507229 100644 (file)
--- a/imp/config/prefs.php.dist
+++ b/imp/config/prefs.php.dist
@@ -1117,10 +1117,7 @@ $_prefs['msgflags'] = array(
 // See the 'msgflags' preference for the format of this value.
 $_prefs['msgflags_user'] = array(
     // 'value' = json_encode(array())
-    'value' => '[]',
-    'locked' => false,
-    'shared' => false,
-    'type' => 'implicit'
+    'value' => '[]'
 );
 
 // The default color to use for flags that don't require row highlighting.