Index: misctools/become
===================================================================
--- misctools/become
+++ misctools/become
@@ -1,6 +1,8 @@
 #!/bin/bash
 #
 # Copyright © 2013 Marc-André Pelletier <mpelletier@wikimedia.org>
+#             2024 Marc-André Pelletier <mpelletier@wikimedia.org>
+#                  Valerio Bozzolan <boz@reyboz.it>
 #
 # Permission to use, copy, modify, and/or distribute this software for any
 # purpose with or without fee is hereby granted, provided that the above
@@ -15,25 +17,46 @@
 # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 #
 
-prefix=$(/bin/cat /etc/wmcs-project)
-if [ $# -lt 1 -o "$1" = "--help" ]; then
-  echo "usage: $(basename $0) <toolname> [command [args...]]" >&2
-  exit 1
+# NOTE: This script relies on the Bash feature "$EUID".
+#       So, the shebang cannot use /bin/sh.
+
+# Be strict. In case of an error, die without proceeding.
+set -e
+
+help() {
+    echo "usage: $(basename "$0") <toolname> [command [args...]]" >&2
+}
+
+# If the user wants help, print usage, then exit successfully.
+if [ "$1" = "--help" ]; then
+    help "$0"
+    exit 0
 fi
+
+# If the command is called without arguments, show the help message, and exit with an error status.
+if [ $# -lt 1 ]; then
+    help "$0"
+    exit 1
+fi
+
+# Get the tool name from the first argument, then discard it from the arguments list.
 tool="$1"
 shift
 
+# Get the prefix applied to the Unix user group of every tool.
+prefix=$(< /etc/wmcs-project)
+
 # Test whether the given tool exists.
 if ! id "$prefix.$tool" >/dev/null 2>&1 || ! [ -d "/data/project/$tool" ]; then
-  echo "$(basename $0): no such tool '$tool'" >&2
-  exit 1
+    echo "$(basename "$0"): no such tool: '$tool'" >&2
+    exit 1
 fi
 
-# Test whether the user is a member of the tool's group in this
-# session unless the user is root.
-if [ $EUID -ne 0 ] && ! echo " $(groups) " | fgrep -q " $prefix.$tool "; then
+# Test whether the user is a member of the tool's group in this session, unless the user is root.
+# TODO: just check whenever you can write in the tool directory.
+if [ $EUID -ne 0 ] && ! echo " $(groups) " | grep --fixed-strings --quiet " $prefix.$tool "; then
     # Test whether the user is a member of the tool's group at all.
-    if echo ",$(getent group "$prefix.$tool" | cut -d : -f 4)," | fgrep -q ",$(id -nu),"; then
+    if echo ",$(getent group "$prefix.$tool" | cut -d : -f 4)," | grep --fixed-strings --quiet ",$(id -nu),"; then
         echo "You were added to the group $prefix.$tool after you started this login session." >&2
         echo "You need to log out and in again to be able to \"become $tool\"." >&2
     else
@@ -45,4 +68,5 @@
 fi
 
 # Execute sudo.
-exec /usr/bin/sudo -niu "$prefix.$tool" "$@"
+# TODO: evaluate the adoption of "-- $@" to separate configuration from main arguments.
+exec /usr/bin/sudo --non-interactive --login --user="$prefix.$tool" "$@"