From e2e440f479e9b01ae4062dcc1f66a020cfe54122 Mon Sep 17 00:00:00 2001
From: Mac Malone <mac@lean-fro.org>
Date: Tue, 10 Jun 2025 05:28:05 +0200
Subject: [PATCH] fix: lake: re-export `LeanOption` from `Lean` in `Lake`

---
 src/lake/Lake/Config/LeanConfig.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/lake/Lake/Config/LeanConfig.lean b/src/lake/Lake/Config/LeanConfig.lean
index 03b09f33f489..845ecc273ecb 100644
--- a/src/lake/Lake/Config/LeanConfig.lean
+++ b/src/lake/Lake/Config/LeanConfig.lean
@@ -13,6 +13,9 @@ open System Lean
 
 namespace Lake
 
+-- 2025-06-08: `LeanOption` was moved to the `Lean` namespace
+export Lean (LeanOption)
+
 /--
 Lake equivalent of CMake's
 [`CMAKE_BUILD_TYPE`](https://stackoverflow.com/a/59314670).