chore: avoid rebuilding leanmanifest in each build (#5057)

leanprover · Aug 15, 2024 · 4d4d485 · 4d4d485
1 parent d1174e1
commit 4d4d485
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
@@ -4,7 +4,8 @@ set_target_properties(leanmain PROPERTIES
   OUTPUT_NAME leanmain)
 
 # library must contain at least one non-manifest file
-file(WRITE ${CMAKE_BINARY_DIR}/temp/empty.c)
+# We use `CONFIGURE` instead of `WRITE` so as to avoid touching the file on each run
+file(CONFIGURE OUTPUT ${CMAKE_BINARY_DIR}/temp/empty.c CONTENT "")
 add_library(leanmanifest STATIC ${CMAKE_BINARY_DIR}/temp/empty.c manifest.rc)
 set_target_properties(leanmanifest PROPERTIES
   ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib/lean