From ff6816a854ef5cf2966519452d03933785f2fdeb Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Wed, 11 Mar 2026 16:51:09 +1100
Subject: [PATCH] fix: avoid duplicate lake test registration when LAKE_CI is
 on (#12877)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR fixes a CMake error when the `lake-ci` label is used. The
previous
implementation appended the full `tests/lake/tests/` glob to a base list
that
already included `tests/lake/tests/shake/test.sh`, causing a duplicate
`add_test` name. This uses an if/else to select the appropriate glob
instead.

Discovered via https://github.com/leanprover/lean4/pull/12540 which has
the
`lake-ci` label.

🤖 Prepared with Claude Code

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>