error output from `lake build`

[Ben-PH]

from running the run-tests.sh:

[3/3] Lean 4 Formal Proofs
------------------------------------------------------------
Running: lake build

✓ No 'sorry' statements found in source files

error: ././.lake/packages/mathlib/lakefile.lean:36:40: error: unexpected token ']'; expected term
error: ././.lake/packages/mathlib/lakefile.lean: package configuration has errors

Build completed successfully
Verified theorems/lemmas: 0
0

============================================================
TEST SUITE COMPLETE
============================================================

I'm not familiar enough with lean4 to know if this is needing of attention or not, but it got pinged, so wanted to flag it.

[Ben-PH]

weird: second run through, no problem. I'll keep this issue open for the time being in case something comes up, or someone that knows more about this can shed some light. My optimistic outlook at this point is this will be closed as a "false positive" issue.