WARNING: deleting a user will completely remove EVERYTHING related to it (including runs, clarifications, etc).
diff --git a/src/optionlower.php b/src/optionlower.php
index fc4b2ded..887d95c1 100644
--- a/src/optionlower.php
+++ b/src/optionlower.php
@@ -127,6 +127,7 @@ function computeHASH()
+
diff --git a/src/team/files.php b/src/team/files.php
index 42fba28c..2792a315 100644
--- a/src/team/files.php
+++ b/src/team/files.php
@@ -116,6 +116,7 @@ function conf2(url) {