1 files changed, 10 insertions, 3 deletions
diff --git a/admin.php b/admin.php
index a93570e43..19c1661ed 100644
--- a/admin.php
+++ b/admin.php
@@ -69,8 +69,10 @@ if (isset($_GET['change_theme']))
 // +-----------------------------------------------------------------------+
 // |                    synchronize user informations                      |
 // +-----------------------------------------------------------------------+
-
-sync_users();
+if (mt_rand(0,9)==0)
+{
+  sync_users();
+}
 
 // +-----------------------------------------------------------------------+
 // |                            variables init                             |
@@ -197,7 +199,6 @@ if (
         'cat_move',     // ?only POST
         'cat_options',  // ?only POST; public/private; lock/unlock
         'cat_perm',     // ?only POST
-        'element_set',  // ?only POST; associate/dissociate
         'picture_modify', // ?only POST; associate/dissociate
         'user_list',    // ?only POST; group assoc
         'user_perm',
@@ -205,6 +206,12 @@ if (
         'group_list',   // delete group
       )
     )
+    or ( isset($_POST) and in_array($page['page'],
+        array(
+          'batch_manager',  // associate/dissociate; delete; set level
+        )
+      )
+    )
   )
 {
   invalidate_user_cache();