chore: add -v flag to lake update in CI (#29338)

Seems no harm to have this information. We only ever look at these logs on failure anyway.

Author: kim-em

.github/workflows/nightly_merge_master.yml

@@ -46,7 +46,7 @@ jobs:
           git merge upstream/master --strategy-option ours --no-commit --allow-unrelated-histories || true
           # We aggressively run `lake update`, to avoid having to do this by hand.
           # When Batteries changes break Mathlib, this will likely show up on nightly-testing first.
-          lake update
+          lake update -v
           git add .
           # If there's nothing to do (because there are no new commits from master),
           # that's okay, hence the '|| true'.

.github/workflows/update_dependencies.yml

@@ -56,7 +56,7 @@ jobs:
 
       - name: Update dependencies
         if: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') }}
-        run: lake update
+        run: lake update -v
 
       - name: Check if lean-toolchain was modified
         if: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') }}

scripts/merge-lean-testing-pr.sh

@@ -29,7 +29,7 @@ if git ls-files -u | grep -q '^'; then
     exit 1
 fi
 
-if ! lake update; then
+if ! lake update -v; then
     echo "Lake update failed. Please resolve conflicts manually."
     git status
     exit 1