Merge #1201: ci: Do not set git's user.{email,name} config options

9b60e31 ci: Do not set git's `user.{email,name}` config options (Hennadii Stepanov)

Pull request description:

  A cleanup after #1199.

  git's `user.{email,name}` config options have been no longer required since 0ecf318.

ACKs for top commit:
  real-or-random:
    utACK 9b60e31

Tree-SHA512: 04f737b0549a91ca992cd1410420e041549a07869eeef068e08971781ea8a4c88a2486e789df36a5ad370ccbbf5d9f7e49ab5f7c1d01faef358ffc4863aaf8e4

Author: real-or-random

.cirrus.yml

@@ -55,8 +55,6 @@ cat_logs_snippet: &CAT_LOGS
 
 merge_base_script_snippet: &MERGE_BASE
   merge_base_script:
-    - git config --global user.email "[email protected]"
-    - git config --global user.name "ci"
     - if [ "$CIRRUS_PR" = "" ]; then exit 0; fi
     - git fetch --depth=1 $CIRRUS_REPO_CLONE_URL "pull/${CIRRUS_PR}/merge"
     - git checkout FETCH_HEAD  # Use merged changes to detect silent merge conflicts