From 0279d29741089d8a26ca0d2ef08229390dc0cf1b Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 21 Mar 2019 12:50:17 +0100
Subject: [PATCH] chore(shell/CMakeLists): add `bin_lean_stage0` target

---
 doc/make/index.md        | 5 ++++-
 src/shell/CMakeLists.txt | 5 +++++
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/doc/make/index.md b/doc/make/index.md
index 42ff59cb33..fa8ac7da21 100644
--- a/doc/make/index.md
+++ b/doc/make/index.md
@@ -97,7 +97,10 @@ Development Workflows
   C++ change. The `lean` target can be used to build the same binary without copying
   it to `bin/`, which can be useful for quickly building a debug version without
   changing the binary used by the editor. The `LEAN_PATH` variable may need to be set
-  to the location of `library/` manually in this case.
+  to the location of `library/` manually in this case. Conversely, if you did a C++
+  change but the stdlib fails to build, you can use the `bin_lean_stage0` target to
+  temporarily use `lean_stage0` as `bin/lean` so that you can fix the stdlib in your
+  editor.
 * When making a parallel change in both Lean and C++, there usually is no simple
   way of writing C++ code that builds in both stage0 and stage1. In this case,
   temporarily set `-DREBUILD_STAGE0=OFF` to deactivate rebuilding `lean_stage0`,
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index c0bb725188..17da6b1937 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -6,6 +6,11 @@ else()
   set_target_properties(lean_stage0 PROPERTIES IMPORTED_LOCATION "${CMAKE_CURRENT_BINARY_DIR}/lean_stage0")
 endif()
 
+ADD_CUSTOM_TARGET(bin_lean_stage0 ALL
+  COMMAND "${CMAKE_COMMAND}" -E copy_if_different "$<TARGET_FILE:lean_stage0>" "${LEAN_SOURCE_DIR}/../bin/lean"
+  DEPENDS lean_stage0
+)
+
 add_custom_target(stdlib
   # '-G Ninja' complains otherwise
   BYPRODUCTS "${CMAKE_BINARY_DIR}/stage1/libleanstdlib.a"