From c0ef6a94910d6f8305b7b84515194b4b96e02175 Mon Sep 17 00:00:00 2001
From: leanprover-community-mathlib4-bot
 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Date: Sun, 20 Oct 2024 00:22:16 +0000
Subject: [PATCH] Trigger CI for https://github.com/leanprover/lean4/pull/5684